% problem-set/algebra/groups/commutator.ver1.in
% created : 07/09/86                                               
% revised : 08/12/88                                          

% description:
%
% Theorem: (commutator thm.) if, for all x in G, x*x*x=e then 
% {{x,y},y}=e, where {x,y}=x*y*inverse(x)*inverse(y) is the
% commutator of x and y.

% 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

set(hyper_res).
set(back_demod).
set(factor).
set(Unit_deletion).
assign(max_kept,5000).


list(axioms).

%  existence of identity    

P(e,x,x).
P(x,e,x).

%  existence of inverse  

P(g(x),x,e).
P(x,g(x),e).

%  closure  

P(x,y,f(x,y)).

%  associative property  

-P(x,y,u) | -P(y,z,v) | -P(u,z,w) | P(x,v,w).
-P(x,y,u) | -P(y,z,v) | -P(x,v,w) | P(u,z,w).

%  the operation is well defined  

-P(x,y,z) | -P(x,y,w) | EQUAL(z,w) .

%  equality axioms  

EQUAL(x,x).
-EQUAL(x,y) | EQUAL(y,x).
-EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z).

%  equality substitution axioms  

-EQUAL(x,y) | -P(x,w,z) | P(y,w,z).
-EQUAL(x,y) | -P(w,x,z) | P(w,y,z).
-EQUAL(x,y) | -P(w,z,x) | P(w,z,y).
-EQUAL(x,y) | EQUAL(f(x,w),f(y,w)).
-EQUAL(x,y) | EQUAL(f(w,x),f(w,y)).
-EQUAL(x,y) | EQUAL(g(x),g(y)).


% x cubed is equal to x 

-P(x,x,y) | P(x,y,e).
-P(x,x,y) | P(y,x,e).

end_of_list.


list(sos).

% denial of the theorem 

P(a,b,c).
P(c,g(a),d).
P(d,g(b),h).
P(h,b,j).
P(j,g(h),k).
-P(k,g(b),e).

end_of_list.


list(demodulators).

EQUAL(g(e),e).
EQUAL(f(x,e),x).
EQUAL(f(e,x),x).
EQUAL(f(x,g(x)),e).
EQUAL(f(g(x),x),e).
EQUAL(g(g(x)),x).

end_of_list.
