% Q:\DIF\ALL.POS         Revised 2000 August 16

clear(symbol_elim).
set(order_eq).
set(sort_literals).
set(unit_deletion).
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([id(x),V,pair(x,x),first(x),second(x),singleton(x),
     union(x,x),cart(x,x),SINGLETON,VERTSECT(x),CUP,
     intersection(x,x),complement(x),D(x),apply(x,x),image(x,x),
     composite(x,x),inverse(x),E,DUP,DIF,FIRST,SECOND,SWAP,
     FUNCTION(x),equal(x,x),member(x,x)]).

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

list(usable).
subclass(x,x).                                                   % PO-1
end_of_list.

formula_list(sos).
%  Definition of the binary function DIF
equal(composite(VERTSECT(intersection(composite(inverse(E),FIRST),
      composite(complement(inverse(E)),SECOND))),id(cart(V,V))),DIF).
%  Corollary DIF-FU
FUNCTION(DIF).
%  Theorem DIF-AP1
(all x (member(x,cart(V,V)) -> equal(apply(DIF,x),
        intersection(first(x),complement(second(x)))))).
%  Theorem DIF-DO
equal(D(DIF),cart(V,V)).
end_of_list.

list(demodulators).
equal(union(x,y),union(y,x)).                                    % U-2
end_of_list.