% Q:\DJ\ALL.POS         Revised 2000 August 19

clear(symbol_elim).
set(order_eq).
set(sort_literals).
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([0,V,singleton(x),union(x,x),cart(x,x),intersection(x,x),
     complement(x),D(x),restrict(x,x,x),notsub(x,x),
     equal(x,x),member(x,x),subclass(x,x),disjoint(x,x)]).

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

formula_list(sos).
%  Definition DJ-DEF of disjoint
(all x y (equal(intersection(x,y),0) <-> disjoint(x,y))).
%  Theorem DJ-ASS
(all x y z (disjoint(intersection(x,y),z) -> disjoint(x,intersection(y,z)))).
%  Theorem DJ-MEM
(all x y z (-member(x,y) | -member(x,z) | -disjoint(y,z))).
%  Theorem DJ-1A
(all x disjoint(x,0)).
%  Theorem DJ-1B
(all x disjoint(0,x)).
%  Theorem DJ-2A
(all x disjoint(x,complement(x))).
%  Theorem DJ-2B
(all x disjoint(complement(x),x)).
%  Theorem DJ-3A
(all x (disjoint(x,x) -> equal(x,0))).
%  Theorem DJ-3B
(all x (equal(x,0) -> disjoint(x,x))).
%  Theorem DJ-4
(all x y (disjoint(x,y) -> disjoint(y,x))).
%  Theorem DJ-5A
(all x y (subclass(x,y) -> disjoint(x,complement(y)))).
%  Theorem DJ-5B
(all x y (disjoint(x,complement(y)) -> subclass(x,y))).
%  Theorem DJ-5C
(all x y (disjoint(x,y) -> subclass(x,complement(y)))).
%  Theorem DJ-6A
(all x y (disjoint(singleton(x),y) -> -member(x,y))).
%  Theorem DJ-6B
(all x y (-member(x,y) -> disjoint(singleton(x),y))).
%  Theorem DJ-7
(all x y z ((disjoint(x,z) & disjoint(y,z))
                      -> disjoint(union(x,y),z))).
%  Theorem DJ-8
(all x y z ((subclass(x,y) & disjoint(y,z)) -> disjoint(x,z))).
%  Theorem DJ-9A
(all x y z (disjoint(x,cart(y,z)) -> equal(restrict(x,y,z),0))).
%  Theorem DJ-9B
(all x y z (equal(restrict(x,y,z),0) -> disjoint(x,cart(y,z)))).
%  Lemma DJ-10A
(all x z ((member(z,V) & -disjoint(x,cart(singleton(z),V))) ->
               member(z,D(x)))).
%  Theorem DJ-10B
(all x z (member(z,D(x)) -> -disjoint(x,cart(singleton(z),V)))).
%  Theorem DJ-10C
(all x z (-disjoint(x,cart(singleton(z),V)) -> member(z,D(x)))).
%  Theorem DJ-C-1
(all x y (disjoint(x,y) | member(notsub(x,complement(y)),x))).
%  Theorem DJ-C-2
(all x y (disjoint(x,y) | member(notsub(x,complement(y)),y))).
%  Theorem DJ-EQ
(all x y ((disjoint(x,y) & subclass(complement(x),y)) 
            -> equal(complement(x),y))).
% Lemma
% equal(notsub(singleton(0),0),0).
end_of_list.

list(demodulators).
equal(intersection(x,y),intersection(y,x)).                      % I-2
end_of_list.