% problem-set/set.theory/naive/subset.ver1.clauses
% created : 07/16/86 
% revised : 08/10/88 

% description:
%
% Theorem: If A and B are contained in C then the union of A and B are also.                                 
% representation:
%
% declare_predicates(2,[EL,INCL,EQ,EQE]).
% declare_functions(2,[difel,join,int]).
% declare_function(1,comp).
% declare_constants([as,bs,cs,ds,empty]).
% declare_variables([x,y,z,xs,ys,zs,xp,yp]).
%
% In the following axioms, EQ(xs,ys) represents Equality of sets,
% EQE(x,y) represents Equality of elements.  difel(xs,ys) represents an 
% element in 'xs' but not in 'ys'.  join(xs,ys) is the union of xs and
% ys; int(xs,ys) is the intersection of xs and ys;  comp(xs) is the
% complement of xs; as, bs, and cs are constant sets; empty is the empty
% set.


% definition of the empty set 

-EL(x,empty).

% axioms of inclusion 

-INCL(xs,ys) | -EL(x,xs) | EL(x,ys).
 INCL(xs,ys) |  EL(difel(xs,ys),xs).
 INCL(xs,ys) | -EL(difel(xs,ys),ys).

% axioms of complementation 

 EL(x,xs)    |  EL(x,comp(xs)).
-EL(x,xs)    | -EL(x,comp(xs)).

% axioms of union 

-EL(x,xs)    |  EL(x,join(xs,ys)).
-EL(x,ys)    |  EL(x,join(xs,ys)).
-EL(x,join(xs,ys))  |  EL(x,xs)  |   EL(x,ys).

% axioms of intersection 

-EL(x,xs)    |  -EL(x,ys)    |  EL(x,int(xs,ys)).
-EL(x,int(xs,ys))  |  EL(x,xs).
-EL(x,int(xs,ys))  |  EL(x,ys).

% set equality axioms 

-EQ(xs,ys)   |  INCL(xs,ys).
-EQ(xs,ys)   |  INCL(ys,xs).
-INCL(xs,ys) | -INCL(ys,xs)  |  EQ(xs,ys).

% equality axioms 

 EQ(xs,xs).
-EQ(xs,ys)   |  EQ(ys,xs).
-EQ(xs,ys)   | -EQ(ys,zs)  |  EQ(xs,zs).
 EQE(x,x).
-EQE(x,y)   |  EQE(y,x).
-EQE(x,y)   | -EQE(y,z)  |  EQE(x,z).

% equality substitution axioms 

-EQE(x,y)   | -EL(x,xs)  |  EL(y,xs).
-EQ(xs,ys)   | -EL(x,xs)  |  EL(x,ys).
-EQ(xs,xp)   | -INCL(xs,ys)  |  INCL(xp,ys).
-EQ(ys,yp)   | -INCL(xs,ys)  |  INCL(xs,yp).
-EQ(xs,xp)   | EQE(difel(xs,ys),difel(xp,ys)).
-EQ(ys,yp)   | EQE(difel(xs,ys),difel(xs,yp)).
-EQ(xs,xp)   | EQ(comp(xs),comp(xp)).
-EQ(xs,xp)   | EQE(join(xs,ys),join(xp,ys)).
-EQ(ys,yp)   | EQE(join(xs,ys),join(xs,yp)).
-EQ(xs,xp)   | EQE(int(xs,ys),int(xp,ys)).
-EQ(ys,yp)   | EQE(int(xs,ys),int(xs,yp)).


% denial of the theorem 

INCL(as,cs).
INCL(bs,cs).
-INCL(join(as,bs),cs).