% problem-set/algebra/rings/minuses.ver2.clauses
% created : 07/09/86
% revised : 07/13/88

% description : 
%
% Theorem : In any ring, for all x, (-x) * (-y) = x * y  [ - indicates
% additive inverse ].

% 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,d,e]).
% 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.


% existence of an additive identity 

S(e,x,x).
S(x,e,x).

% closure property 

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

% existence of inverses 

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

% associative property 

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

% commutative property 

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

% distributive property 

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

EQUAL(x,x).

% equality substitution axioms 

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

-EQUAL(x,y) |  -S(x,w,z)    |  S(y,w,z).
-EQUAL(x,y) |  -S(w,x,z)    |  S(w,y,z).
-EQUAL(x,y) |  -S(w,z,x)    |  S(w,z,y).
-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).

% the operations are well defined 

-EQUAL(x,y) |   EQUAL(g(x),g(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(j(x,w),j(y,w)).
-EQUAL(x,y) |   EQUAL(j(w,x),j(w,y)).

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


% the denial of the theorem 

P(a,b,c).
P(g(a),g(b),d).
-EQUAL(c,d).

% lemmas

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