% problem-set/algebra/groups/Group.ax.g.clauses
% created : 07/22/86                     
% revised : 08/15/88                     

% description:
%
% The following are the usual axioms of a group with an additional argument 
% in the usual predicates and functions to identify the group.

% representation:
%
% declare_predicates(2,[EL,EQUAL]).
% declare_predicate(4,[P]).
% declare_functions(1,[e,k,r,s,p1,p2,p3,q1,q2,q3]).
% declare_functions(2,[g,m]).
% declare_function(3,[f]).
% declare_constants([a,b,c,d,i,h,j,d1,d2,d3,G,G1,G2]).
% declare_variables([x,y,z,w,xg,yg,xy,yz,xyz]).
%
% EL(x,y) : x is an element of group y
% P(x,y,z,w) : in group x, the product of y and z is w
% e(x) : names the identity element of group x
% k(x) : names an isomorphism (see order2.ver3, order3.ver3)
% r(x) : is a possible isomorphism (see order2.ver4)
% s(x) : is a possible isomorphism (see order2.ver4)
% p1(x) : is a possible isomorphism (see order3.ver4)
% p2(x) : is a possible isomorphism (see order3.ver4)
% p3(x) : is a possible isomorphism (see order3.ver4)
% q1(x) : is a possible isomorphism (see order3.ver4)
% q2(x) : is a possible isomorphism (see order3.ver4)
% q3(x) : is a possible isomorphism (see order3.ver4)
% g(x,y) : in group x, names inverse of y
% m(x,y) : in group x, names an element which does not equal any power of
%	y; (see cyclic)
% f(x,y,z) : in group x, names the product of y and z
% i : identity element in group G named


%  closure property 

-EL(x,xg)  | -EL(y,xg)  |  P(xg,x,y,f(xg,x,y)).
-EL(x,xg)  | -EL(y,xg)  |  EL(f(xg,x,y),xg).

%  the operation is well defined 

-P(xg,x,y,z)  | -P(xg,x,y,w)  |  EQUAL(w,z).
-P(xg,x,z,y)  | -P(xg,x,w,y)  |  EQUAL(w,z).
-P(xg,z,y,x)  | -P(xg,w,y,x)  |  EQUAL(w,z).

%  existence of identity 

EL(e(xg),xg).
P(xg,e(xg),x,x).
P(xg,x,e(xg),x).

%  existence of inverses 

-EL(x,xg)  |  EL(g(xg,x),xg).
P(xg,g(xg,x),x,e(xg)).
P(xg,x,g(xg,x),e(xg)).

%  associative property 

-P(xg,x,y,xy)  | -P(xg,y,z,yz)  | -P(xg,xy,z,xyz)  |  P(xg,x,xy,xyz).
-P(xg,x,y,xy)  | -P(xg,y,z,yz)  | -P(xg,x,yz,xyz)  |  P(xg,xy,z,xyz).

%  equality axioms 

EQUAL(x,x).
-EQUAL(x,y)  |  EQUAL(y,x).
-EQUAL(x,y)  | -EQUAL(y,z)  |  EQUAL(x,z).

%  equality substitution axioms 

-EQUAL(xg,yg)| -P(xg,x,y,z)  |  P(yg,x,y,z).
-EQUAL(x,y)  | -P(xg,x,z,w)  |  P(xg,y,z,w).
-EQUAL(x,y)  | -P(xg,w,x,z)  |  P(xg,w,y,z).
-EQUAL(x,y)  | -P(xg,w,z,x)  |  P(xg,w,z,y).
-EQUAL(xg,yg)|  EQUAL(f(xg,x,y),f(yg,x,y)).
-EQUAL(x,y)  |  EQUAL(f(xg,x,z),f(xg,y,z)).
-EQUAL(x,y)  |  EQUAL(f(xg,z,x),f(xg,z,y)).
-EQUAL(xg,yg)|  EQUAL(g(xg,x),g(yg,x)).
-EQUAL(x,y)  |  EQUAL(g(xg,x),g(xg,y)).
-EQUAL(xg,yg)| -EL(x,xg)  |  EL(x,yg).
-EQUAL(x,y)  | -EL(x,xg)  |  EL(y,xg).
-EQUAL(xg,yg)|  EQUAL(e(xg),e(yg)).