% problem-set/algebra/rings/Ring.lemmas.clauses 
% created : 07/07/86                   
% revised : 07/13/88               

% description :
%
% The following are established lemmas 

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

% Cancellation Laws                   

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

% established by 'zero.ver2' : 

P(a,0,0).

% established by 'minuses.ver2' :

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

% established by 'lemma.ver ' :

EQUAL(g(x),x).