% problem-set/algebra/groups/Lemmas.p.clauses
% created : 08/26/86                    
% revised : 08/11/88                    

% description:
%
% The following identities may be established 

% representation:
%
% declare_predicate(1,[O]).
% declare_predicate(2,[EQUAL]).
% declare_predicate(3,[P]).
% declare_functions(1,[g,k]).
% declare_functions(2,[f,l]).
% declare_constants([e,a,b,c,d,h,j,k]).
% declare_variables([x,y,z,u,v,w]).
%
% O(x) : used for membership in a subgroup of index 2 (see index)
% P(x,y) : product of x and y is z
% g(x) : inverse of x
% k(x) : used to name some inverse of x (see ident2)
% f(x,y) : names the product of x and y
% l(x,y) : names an element of the subgroup of index 2 (see index)
% e : identity element


% inverse of inverse of x is equal to x       

EQUAL(g(g(x)),x).

% inverse of identity is identity             

EQUAL(g(e),e).