% problem-set/algebra/groups/xsquared.ver2.in % created : 07/21/86 % revised : 08/12/88 % description: % % Theorem: if, for all x in G, x*x=e then G is abelian (commutative); % i.e., for all x,y in G, x*y=y*x. % representation: % % declare_predicate(1,[O]). % declare_predicate(2,[EQUAL]). % declare_function(1,[g]). % declare_functions(2,[f,l]). % declare_constants([e,a,b,c,d,h,j,k]). % declare_variables([x,y,z]). % % O(x) : membership in a subgroup of index 2 (see index) % g(x) : inverse of x % f(x,y) : names the product of x and y % l(x,y) : names an element in O (see index) % e : identity element set(para_into). set(para_from). set(para_from_left). set(para_from_right). set(back_demod). set(UR_res). assign(max_kept,5000). list(axioms). % For any x and y in the group x*y is also in the group. No clause is needed % here since this is an instance of reflexivity given as EQUAL(x,x). % There exists an identity element 'e' defined below. % left identity EQUAL(f(e,x),x). % right identity EQUAL(f(x,e),x). % For any x in the group, there exists an element y such that x*y = y*x = e. % left inverse EQUAL(f(g(x),x),e). % right inverse EQUAL(f(x,g(x)),e). % The operation '*' is associative EQUAL(f(f(x,y),z),f(x,f(y,z))). % The operation '*' is well-defined. No clause is needed here since this % is an instance of reflexivity given as EQUAL(x,x). % reflexivity EQUAL(x,x). end_of_list. list(sos). % Denial of theorem : % If x**2 = e for all x, then the group is commutative EQUAL(f(x,x),e). EQUAL(f(a,b),c). -EQUAL(f(b,a),c). end_of_list. list(demodulators). EQUAL(g(e),e). EQUAL(g(g(x)),x). end_of_list.