% Q:\CROSS\ALL.POS         Revised 2000 August 7

clear(symbol_elim).
set(order_eq).
set(sort_literals).
% set(factor).
set(dynamic_demod_all).
set(back_demod).
set(process_input).
clear(print_given).
set(print_lists_at_end).

set(lrpo).
set(lex_order_vars).
lex([V,pair(x,x),first(x),second(x),cart(x,x),CROSS,IMAGE(x),CART,
     cross(x,x),D(x),apply(x,x),composite(x,x),TWIST,
     FUNCTION(x),equal(x,x),member(x,x)]).

assign(max_mem,300).
assign(stats_level,0).

list(usable).
%subclass(x,x).                                                   % PO-1
equal(x,x).                                                      % EQ-1
%subclass(cart(x,y),cart(V,V)).                                   % CP-1
end_of_list.

formula_list(sos).
%  Definition DEF-CRS of the binary function CROSS
equal(composite(IMAGE(TWIST),CART),CROSS).
%  Theorem CRS-FU
FUNCTION(CROSS).
%  Theorem CRS-DO
equal(D(CROSS),cart(V,V)).
%  Theorem CRS-AP1
(all x (member(x,cart(V,V)) -> 
        equal(apply(CROSS,x),cross(first(x),second(x))))).
%  Corollary CRS-AP2
(all x y (member(pair(x,y),cart(V,V)) -> 
          equal(apply(CROSS,pair(x,y)),cross(x,y)))).
end_of_list.

list(demodulators).
%equal(intersection(x,y),intersection(y,x)).                      % I-2
%equal(intersection(x,complement(x)),0).                          % C-3A
%equal(union(x,y),union(y,x)).                                    % U-2
%equal(union(0,x),x).                                             % U-4
%equal(cart(0,x),0).                                              % CP-3B
%equal(composite(union(x,y),z),
%     union(composite(x,z),composite(y,z))).                      % CO-U1
%equal(composite(x,union(y,z)),
%     union(composite(x,y),composite(x,z))).                      % CO-U2
%equal(composite(cart(x,y),id(z)),cart(intersection(x,z),y)).     % new!
end_of_list.