% problem-set/algebra/rings/zero.ver1.clauses % created : 07/09/86 % revised : 07/13/88 % description : % % Theorem : In any ring, for all x, (x * 0) = 0 [ 0 is the additive % identity ]. % representation : % % declare_predicated(3,[S,P]). % declare_predicate(2,EQUAL). % declare_functions(2,[j,f]). % declare_function(1,g). % declare_constants([a,e]). % declare_variables([x,y,z,w,v,v0,v1,v2,v3,v4]). % % S means sum, P means product, e is the additive identity, a is a % constant element of the ring, g(x) is the additive inverse of x, % j(x,y) is the sum of x and y, and f(x,y) is the product of x and y. % 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,e,e).