Quelle  zp_group.pvs

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


zp_group[n:posnat]: THEORY

BEGIN


  IMPORTING algebra@group
  

   Zn: set[below(n)] = {m: nat | m < n};

  ++(a,b: below(n)): below(n) = rem(n)(a+b)

   Zn_group: LEMMA group?[below(n), ++, 0](Zn)

   Zn_finite: LEMMA is_finite(Zn)

   Zn_card: LEMMA card(Zn) = n


END zp_group