%% Clause labels found in directory Q:\FS
% FS-PC-1
-FUNCTION(x) | subclass(P(x),FUNS).
% FS-RS1
-FUNCTION(z) | -member(x,V) | member(restrict(z,x,y),FUNS).
% FS-FU
-FUNCTION(z) | -member(z,V) | member(z,FUNS).
% HO-1
-HOM(xh1,xf1,xf2) | -HOM(xh2,xf2,xf3) | HOM(composite(xh2,xh1),xf1,xf3).
% FS-RP-1
-member(FUNS,x).
% FS-4
-member(x,FUNS) | -member(x,fix(composite(E, composite(cross(Id,complement(Id)),inverse(E))))).
% FS-6
-member(x,FUNS) | FUNCTION(x).
% FS-5
-member(x,FUNS) | disjoint(cart(x,x),cross(Id,complement(Id))).
% FS-3
-member(x,FUNS) | subclass(x,cart(V,V)).
% SW-1ST
-member(x,cart(V,V)) | equal(first(swap(x)),second(x)).
% SW-2ND
-member(x,cart(V,V)) | equal(second(swap(x)),first(x)).
% FS-SS
-member(x,cart(V,V)) | member(singleton(x),FUNS).
% FS-PC-2
-subclass(P(x),FUNS) | FUNCTION(x).
% PC-4C
equal(P(V),V).
% FS-SC
equal(U(FUNS),cart(V,V)).
% SW-IN
equal(inverse(SWAP),SWAP).
% RL-3B
equal(inverse(inverse(E)),E).
% SR-IN
equal(inverse(inverse(S)),S).
% RL-3A
equal(inverse(inverse(inverse(x))),inverse(x)).
% SP-8B
equal(pairset(V,y),singleton(y)).
% SP-8A
equal(pairset(x,V),singleton(x)).
% SR-1-COR
equal(restrict(S,V,V),S).
% FS-RP-2
equal(singleton(FUNS),0).
% FS-0
member(0,FUNS).
% FS-1
subclass(FUNS,P(cart(V,V))).
% FS-2
subclass(U(FUNS),cart(V,V)).