% problem-set/algebra/rings/commute.ver2
% created : 07/11/86                                        
% revised : 07/13/88                                        

% description :
%
% Theorem: If for all x, (x * x = x) then the ring 
%         is commutative under multiplication.                   
%         That is, (x * y = y * x) for all x and y.              

% representation :
%
% declare_predicate(2,EQUAL).
% declare_functions(2,[j,f]).
% declare_function(1,g).
% declare_constants([0]).
% declare_variables([x,y,z]).
%
% j(x,y) is the sum of x and y, f(x,y) is the product of x and y; 
% g(x) is the additive inverse of x; 0 is the additive identity element


% The following clauses are given by Stickel as a complete set 
% of reductions for ring theory. 


% existence of left identity for addition 

EQUAL(j(0,x),x).

% existence of left additive inverse  

EQUAL(j(g(x),x),0).

% distributive property of product over sum    

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

% inverse of identity is identity 

EQUAL(g(0),0).

% inverse of inverse of x is x itself 

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

% behavior of 0 and the multiplication operation  

EQUAL(f(x,0),0).
EQUAL(f(0,x),0).

% inverse of (x + y) is inverse(x) + inverse(y)  

EQUAL(g(j(x,y)),j(g(x),g(y))).

% x * inverse(y) = inverse (x * y)

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

% end of Stickel's clauses

% associativity of addition

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

% commutativity of addition

EQUAL(j(x,y),j(y,x)).

% associativity of product

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

% equality 

EQUAL(x,x).

% the ring is boolean

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

% right identity & inverse

EQUAL(j(x,0),x).
EQUAL(j(x,g(x)),0).

% denial of the theorem

EQUAL(f(a,b),c).
-EQUAL(f(b,a),c).

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