% problem-set/algebra/rings/lemma.ver1.clauses
% created : 07/11/86                                        
% revised : 07/13/88                                        

% description :
%
% Theorem: If for all x, (x * x = x) then x + x = 0.

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


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

% beginning of Stickel's clauses
                                                                
% Left identity 

S(0,x,x).

% Left inverse 

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

% Distributivity of product over sum 

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

% inverse of 0 is 0

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

% inverse of inverse of x is x

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

% behavior of 0 and multiplication

P(x,0,0).
P(0,x,0).

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

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

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

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

% end of Stickel's clauses


% Right identity 
S(x,0,x).

% Right inverse 
S(x,g(x),0).

% Associativity 
-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 
S(x,y,j(x,y)).

% Well-definedness of addition 
-S(x,y,u) | -S(x,y,v) | EQUAL(u,v).

% Reflexivity of equality 
EQUAL(x,x).

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

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

% Equality substitution 
-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(j(u,x),j(v,x)).
-EQUAL(u,v) |  EQUAL(j(x,u),j(x,v)).
-EQUAL(u,v) |  EQUAL(g(u),g(v)).

% Addition is commutative 
-S(x,y,z)   | S(y,x,z).

% Associativity of product 
-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) .

% Product is well-defined 
-P(x,y,u) | -P(x,y,v) | EQUAL(u,v).

% Closure of product 
P(x,y,f(x,y)).

% Equality substitution (for the added predicates and functions) 
-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 (x * x = x) 

P(x,x,x).

% denial of the theorem 

-EQUAL(j(a,a),0).

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