% Q:\CUT\AGENDA.TXT          12-04-1997
% Conjectured theorems about IMAGE(id(x)).

formula_list(sos).
%  Theorem CUT-CO
(all x equal(composite(IMAGE(id(x)),inverse(IMAGE(id(x)))),id(P(x)))).
%  Theorem CUT-AP
(all x y (member(x,V) -> equal(apply(IMAGE(id(y)),x),intersection(x,y)))).
%  Theorem CUT-D
(all x y z (member(pair(x,y),cart(V,V)) ->
      member(pair(union(x,y),union(intersection(x,z),intersection(y,z))),
      IMAGE(id(z))))).
%  Lemma CUT-SR-1
(all x y z (member(pair(x,y),composite(S,IMAGE(id(z)))) ->
           subclass(intersection(x,z),y))).
%  Theorem CUT-SR
(all x equal(composite(IMAGE(id(x)),S),composite(S,IMAGE(id(x))))).
%  Theorem CUT-E
(all x equal(composite(id(x),inverse(E)),composite(inverse(E),IMAGE(id(x))))).
%  Theorem CUT-SC
(all x y equal(U(image(IMAGE(id(x)),y)),intersection(x,U(y)))).
%  Theorem CUT-CP
(all x (member(x,V) -> member(pair(x,composite(Id,x)),IMAGE(id(cart(V,V)))))).
end_of_list.