% problem-set/algebra/rings/minuses.ver1.in % created : 07/09/86 % revised : 07/12/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. set(UR_res). assign(max_kept,1000). list(axioms). % 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). end_of_list. list(sos). % the denial of the theorem P(a,b,c). P(g(a),g(b),d). -EQUAL(c,d). end_of_list.