%% Clause labels found in directory Q:\cup
% CUP-OP3A
-member(pair(pair(x,y),z),CUP) | equal(union(x,y),z).
% CUP-OP2
-member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S))) | subclass(union(x,y),z).
% CUP-OP3B
-member(pair(x,y),CUP) | equal(union(first(x),second(x)),y).
% CUP-OP4
-member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)),CUP).
% CUP-OP1
-member(x,V) | -subclass(union(y,z),x) | member(pair(pair(y,z),x),composite(inverse(DUP),cross(S,S))).
% CUP-OP1
-subclass(union(x,y),z) | -member(z,V) | member(pair(pair(x,y),z),composite(inverse(DUP),cross(S,S))).
% CUP-FU
FUNCTION(CUP).
% CUP-DO
equal(D(CUP),cart(V,V)).
% DEF-CUP
equal(PSM(composite(inverse(DUP),cross(S,S))),CUP).
% U-2
equal(union(x,y),union(y,x)).
% CUP-1
subclass(CUP,cart(V,V)).
% CUP-2
subclass(CUP,cart(cart(V,V),V)).
% CUP-3
subclass(D(CUP),cart(V,V)).
% CUP-DUP1
subclass(inverse(DUP),CUP).