% problem-set/algebra/groups/invers2.ver1.in % created : 07/09/86 % revised : 08/11/88 % description: % % Theorem: the right inverse axiom is dependant on the rest of the % axiom set; i.e., each element has a right inverse. % % Note: the axioms P(x,e,x) and P(x,g(x),e) must be deleted. % representation: % % declare_predicate(1,[O]). % declare_predicate(2,[EQUAL]). % declare_predicate(3,[P]). % declare_functions(1,[g,k]). % declare_functions(2,[f,l]). % declare_constants([e,a,b,c,d,h,j,k]). % declare_variables([x,y,z,u,v,w]). % % O(x) : used for membership in a subgroup of index 2 (see index) % P(x,y) : product of x and y is z % g(x) : inverse of x % k(x) : used to name some inverse of x (see ident2) % f(x,y) : names the product of x and y % l(x,y) : names an element of the subgroup of index 2 (see index) % e : identity element set(UR_res). set(back_demod). set(factor). set(Unit_deletion). assign(max_kept,5000). list(axioms). % existence of identity P(e,x,x). % P(x,e,x). DELETED DUE TO THEOREM % existence of inverse P(g(x),x,e). % P(x,g(x),e). DELETED DUE TO THEOREM % closure P(x,y,f(x,y)). % associative property -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). % the operation is well defined -P(x,y,z) | -P(x,y,w) | EQUAL(z,w) . % equality axioms EQUAL(x,x). -EQUAL(x,y) | EQUAL(y,x). -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). % equality substitution axioms -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). -EQUAL(x,y) | EQUAL(f(x,w),f(y,w)). -EQUAL(x,y) | EQUAL(f(w,x),f(w,y)). -EQUAL(x,y) | EQUAL(g(x),g(y)). end_of_list. list(sos). % denial of the theorem -P(a,y,e). end_of_list.