%  problem-set/algebra/category.theory/p1.ver1.clauses
%  created : 07/09/86 
%  revised : 07/07/89 

% description:
%
%  Theorem 1 : If xy is a monomorphism, then y is a monomorphism. 

% representation:
%
% declare_predicate(3,P).
% declare_predicates(2,[DEF,EQUAL]).
% declare_predicate(1,IDENT).
% declare_functions(1,[dom,cod]).   
% declare_function(2,star).
% declare_constants([a,b,c,d,g,h]).
% declare_variables([w,x,y,z,xy,yz,xyz,u,v,w]).
%
% IDENT(x) : x is an identity map 
% DEF(x,y) : the composition xy is defined 
% P(a,b,c) : identifies c as a composition (product) of a and b 
% dom(x) and cod(x) : functions to indicate domain and range of x 
%	note that these are treated as functions, not objects, i.e. 
%	dom(x) is the identity map on the domain of x 
% star(x,y) : skolem function from (all x all y (DEF(x,y) -> 
%	exists z (P(x,y,z)))).
% note that there are no special constants here; they're all used as
%	skolem constants in the denials of theorems


%  composition is closed when defined                              

-DEF(x,y) | P(x,y,star(x,y)).

%  associative property 

-P(x,y,z) | DEF(x,y).
-P(x,y,xy) | -DEF(xy,z) | DEF(y,z).

%  special category theory axiom

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

%  properties of dom(x) and cod(x)

IDENT(dom(x)).
IDENT(cod(x)).
DEF(x,dom(x)).
DEF(cod(x),x).
P(x,dom(x),x).
P(cod(x),x,x).

%  definition of the identity predicate

-DEF(x,y) | -IDENT(x) | P(x,y,y).
-DEF(x,y) | -IDENT(y) | P(x,y,x).

%  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,z,w) | P(y,z,w).
% -EQUAL(x,y) | -P(z,x,w) | P(z,y,w).
% -EQUAL(x,y) | -P(z,w,x) | P(z,w,y).
% -EQUAL(x,y) | EQUAL(dom(x),dom(y)).
% -EQUAL(x,y) | EQUAL(cod(x),cod(y)).
% -EQUAL(x,y) | -IDENT(x) | IDENT(y).
% -EQUAL(x,y) | -DEF(x,z) | DEF(y,z).
% -EQUAL(x,y) | -DEF(z,x) | DEF(z,y).
% -EQUAL(x,y) | EQUAL(star(z,x),star(z,y)).
% -EQUAL(x,y) | EQUAL(star(x,z),star(y,z)).

%  composition is well defined

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


%  Denial of the theorem 

P(a,b,c).
-P(c,x1,x2) | -P(c,x3,x2) | EQUAL(x1,x3).
P(b,h,d).
P(b,g,d).
-EQUAL(h,g).

% lemmas (used as demodulators)

EQUAL(dom(dom(x)),dom(x)).
EQUAL(cod(dom(x)),dom(x)).
EQUAL(dom(cod(x)),cod(x)).
EQUAL(cod(cod(x)),cod(x)).
EQUAL(star(cod(x),x),x).
EQUAL(star(x,dom(x)),x).
EQUAL(star(cod(x),cod(x)),cod(x)).
EQUAL(star(dom(x),dom(x)),dom(x)).
EQUAL(dom(star(x,y)),dom(y)).
EQUAL(cod(star(x,y)),cod(x)).