group_rew[T:Type+,*:[T,T->T],one:T]: THEORY

BEGIN
   ASSUMING IMPORTING group_def[T,*,one]

       fullset_is_group: ASSUMPTION group?(fullset[T])

   ENDASSUMING

   IMPORTING group[T,*,one]

   S,R:       VAR set[T]
   H,G:       VAR group
   a,b,x,y,z: VAR T
   m:         VAR nat
   i,j:       VAR int

   inv_left      : LEMMA inv(x) * x = one 
   inv_right     : LEMMA x * inv(x) = one 
   inv_inv       : LEMMA inv(inv(x)) = x 
   inv_one       : LEMMA inv(one) = one
   inv_in        : LEMMA FORALL (a:(G)): G(inv(a))

   expt_0        : LEMMA a^0                = one
   expt_1        : LEMMA a^1                = a
   expt_m1       : LEMMA a^(-1)             = inv(a)
   one_expt      : LEMMA one^i              = one
 

   one_left      : LEMMA one * x = x
   one_right     : LEMMA x * one = x

END group_rew