% problem-set/algebra/rings/commute.ver4.clauses
% created : 07/09/86                                               
% revised : 07/13/88                                          
                                                                  
% description : 
%
% Theorem: If for all x, (x * x) = x, then the ring is commutative
% under multiplication; i.e., for all x and y, (x * y) = (y * x).

% representation :
%
% S means sum, P means product; 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; a,b,c,d are constant ring elements.
%
% declare_predicates(3,[S,P]).
% declare_predicate(2,EQUAL).
% declare_functions(2,[j,f]).
% declare_function(1,g).
% declare_constants([0,a,b,c,d]).
% declare_variables([x,y,z,u,v,w,v1,v2,v3,v4]).

% Left identity 

S(0,x,x).

% Right identity 

S(x,0,x).

% Left inverse 

S(g(x),x,0).

% Right inverse 

S(x,g(x),0).

% Associative property 

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

% Closure property 

S(x,y,j(x,y)).

% Well definedness of addition 

-S(x,y,u)  | -S(x,y,v) | EQUAL(u,v).

% Addition is commutative 

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

% 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).

% Closure of multiplication 

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

% Well definedness of multiplication 

-P(x,y,u)   |  -P(x,y,v)    |  EQUAL(u,v).

% Distributivity axioms 

-P(x,y,v1)  |  -P(x,z,v2) |  -S(y,z,v3)  | -P(x,v3,v4)  | S(v1,v2,v4).
-P(x,y,v1)  |  -P(x,z,v2) |  -S(y,z,v3)  | -S(v1,v2,v4) | P(x,v3,v4).
-P(y,x,v1)  |  -P(z,x,v2) |  -S(y,z,v3)  | -P(v3,x,v4)  | S(v1,v2,v4).
-P(y,x,v1)  |  -P(z,x,v2) |  -S(y,z,v3)  | -S(v1,v2,v4) | P(v3,x,v4).

% Reflexivity 

EQUAL(x,x).

% Symmetry 

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

% Transitivity 

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

% Equality substitution axioms 

-EQUAL(u,v) |  -S(u,x,y)   |  S(v,x,y).
-EQUAL(u,v) |  -S(x,u,y)   |  S(x,v,y).
-EQUAL(u,v) |  -S(x,y,u)   |  S(x,y,v).
-EQUAL(u,v) |   EQUAL(g(u),g(v)).
-EQUAL(u,v) |   EQUAL(j(u,x),j(v,x)).
-EQUAL(u,v) |   EQUAL(j(x,u),j(x,v)).

-EQUAL(u,v) |  -P(u,x,y)  |  P(v,x,y).
-EQUAL(u,v) |  -P(x,u,y)  |  P(x,v,y).
-EQUAL(u,v) |  -P(x,y,u)  |  P(x,y,v).

-EQUAL(u,v) |   EQUAL(f(u,x),f(v,x)).
-EQUAL(u,v) |   EQUAL(f(x,u),f(x,v)).


% the ring is boolean

P(x,x,x).

% denial of the theorem

P(a,b,c).
-P(b,a,c).

% lemmas

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