% problem-set/algebra/rings/lemma.ver1.in % 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. lex(j(x,x),f(x,x),g(x),0,a,b,c). set(hyper_res). assign(max_kept,1000). assign(max_weight,1000). list(axioms). % 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)). end_of_list. list(sos). % the ring is boolean (x * x = x) P(x,x,x). % denial of the theorem -EQUAL(j(a,a),0). end_of_list. list(demodulators). EQUAL(j(0,x),x). EQUAL(j(g(x),x),0). EQUAL(f(x,j(y,z)),j(f(x,y),f(x,z))). EQUAL(f(j(x,y),z),j(f(x,z),f(y,z))). EQUAL(g(0),0). EQUAL(g(g(x)),x). EQUAL(f(x,0),0). EQUAL(f(0,x),0). EQUAL(g(j(x,y)),j(g(x),g(y))). EQUAL(f(x,g(y)),g(f(x,y))). EQUAL(f(g(x),y),g(f(x,y))). EQUAL(j(j(x,y),z),j(x,j(y,z))). EQUAL(f(f(x,y),z),f(x,f(y,z))). EQUAL(j(x,y),j(y,x)). EQUAL(f(x,x),x). EQUAL(j(x,j(y,z)),j(y,j(x,z))). end_of_list.