%%----------------------------------------------------------------
%%                                                                          
%% Author          : André Luiz Galdino 
%%                   Universidade Federal de Goiás - Brasil
%%                    
%% Last Modified On: November 28, 2011
%%                                                                          
%%----------------------------------------------------------------


class_equation_scaf[D, T:TYPE]: THEORY

BEGIN


   IMPORTING algebra@lagrange_scaf[T], 
             sigma_set@sigma_set[finite_set[T]] 
 

      FP:  VAR finite_partition
       A: VAR finite_set[D]
       B: VAR finite_set[T]
m, n, x : VAR int



card_rest_aux: LEMMA nonempty?(FP) IMPLIES 
                       card(Union(FP)) = card(choose(FP)) + card(Union(rest(FP)))
 

card_partition: LEMMA (nonempty?(FP) AND FORALL (A: (FP)): card(A) /= 0) IMPLIES 
                             card(Union(FP)) = sigma_set.sigma(FP, card)


divide_sigma: LEMMA (nonempty?(FP) AND 
                          FORALL (A: (FP)): card(A) /= 0 AND divides(n, card(A))) IMPLIES 
                             divides(n,sigma_set.sigma(FP, card))

END class_equation_scaf