%  problem-set/algebra/groups/xsquared.ver2.clauses
%  created : 07/21/86                                  
%  revised : 08/12/88                             

% description:
%
% Theorem: if, for all x in G, x*x=e then G is abelian (commutative);
% i.e., for all x,y in G, x*y=y*x.

% representation:
%
% declare_predicate(1,[O]).
% declare_predicate(2,[EQUAL]).
% declare_function(1,[g]).
% declare_functions(2,[f,l]).
% declare_constants([e,a,b,c,d,h,j,k]).
% declare_variables([x,y,z]).
%
% O(x) : membership in a subgroup of index 2 (see index)
% g(x) : inverse of x
% f(x,y) : names the product of x and y
% l(x,y) : names an element in O (see index)
% e : identity element


% For any x and y in the group x*y is also in the group.  No clause is needed 
% here since this is an instance of reflexivity given as EQUAL(x,x).                   
% There exists an identity element 'e' defined below.   
% left identity  

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

% right identity 

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

% For any x in the group, there exists an element y such that x*y = y*x = e. 
% left inverse 

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

% right inverse 

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

% The operation '*' is associative  

EQUAL(f(f(x,y),z),f(x,f(y,z))).

% The operation '*' is well-defined.  No clause is needed here since this 
% is an instance of reflexivity given as EQUAL(x,x).                           

% reflexivity 

EQUAL(x,x).


%  Denial of theorem : 
%  If x**2 = e for all x, then the group is commutative             

EQUAL(f(x,x),e).
EQUAL(f(a,b),c).
EQUAL(f(b,a),c).