% Q:\DEDEKIND\ALL.POS         2000 June 12
% Theorems about Dedekind finite sets

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,id(x),Id,omega,FINITE,DEDEKIND,Q,pair(x,x),singleton(x),
     cart(x,x),intersection(x,x),complement(x),fix(x),D(x),R(x),
     image(x,x),composite(x,x),K,PS,inverse(x),
     ONEONE(x),equal(x,x),member(x,x),subclass(x,x)]).

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

list(usable).
subclass(x,x).                                                   % PO-1
equal(x,x).                                                      % EQ-1
disjoint(x,complement(x)).                                       % DJ-2A
subclass(id(x),Id).                                              % IDX-2
end_of_list.

formula_list(sos).
%  Definition DEF-DK of the class of Dedekind-finite sets
equal(complement(fix(composite(Q,PS))),DEDEKIND).
%  Theorem DK-C-OM
-member(omega,DEDEKIND).
%  Theorem DK-C-DF
equal(fix(composite(Q,PS)),complement(DEDEKIND)).
%  Theorem DK-MEM-1
(all x y ((member(x,DEDEKIND) & member(pair(x,y),Q) & subclass(x,y))
           -> equal(x,y))).
%  Theorem DK-MEM-2
(all x y ((member(x,DEDEKIND) & member(pair(x,y),Q) & subclass(y,x))
           -> equal(x,y))).
%  Theorem DK-PIG
(all x ((ONEONE(x) & subclass(R(x),D(x)) & member(D(x),DEDEKIND))
         -> equal(R(x),D(x)))).
%  Theorem DK-K
subclass(image(K,DEDEKIND),DEDEKIND).
%  Theorem DK-K-IN
subclass(image(inverse(K),DEDEKIND),DEDEKIND).
%  Theorem DK-Q
equal(image(Q,DEDEKIND),DEDEKIND).
%  Theorem DK-0
member(0,DEDEKIND).
%  Corollary DK-FIN
subclass(FINITE,DEDEKIND).
%  Lemma DK-OM-Q1
subclass(intersection(Q,cart(omega,omega)),Id).
%  Theorem DK-OM-Q2
equal(intersection(Q,cart(omega,omega)),id(omega)).
%  Theorem DK-SS
(all x member(singleton(x),DEDEKIND)).
end_of_list.

list(demodulators).
equal(intersection(x,y),intersection(y,x)).                      % I-2
equal(complement(complement(x)),x).                              % C-1
equal(union(x,y),union(y,x)).                                    % U-2
end_of_list.