% Q:\AX-E\ALL.POS         Revised 2001 May 7

clear(symbol_elim).
set(order_eq).
set(sort_literals).
set(unit_deletion).
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([0,id(x),Id,V,Q,BIJ,FUNS,pair(x,x),singleton(x),union(x,x),cart(x,x),U(x),P(x),
     SINGLETON,VERTSECT(x),IMAGE(x),intersection(x,x),complement(x),fix(x),
     D(x),R(x),apply(x,x),image(x,x),CHOICE,composite(x,x),S,DISJOINT,inverse(x),E,
     AxCh,ONEONE(x),FUNCTION(x),equal(x,x),member(x,x),subclass(x,x)]).

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

formula_list(sos).
%  Theorem AC-IM-SC
AxCh -> (all x subclass(image(CHOICE,x),U(x))).
%  Theorem AC-VS
AxCh -> (all x subclass(composite(CHOICE,VERTSECT(x)),x)).
%  Theorem AC-VS-DO
AxCh -> (all x equal(D(composite(CHOICE,VERTSECT(x))),
                     intersection(D(x),D(VERTSECT(x))))).
%  Theorem AC-FS-CO
AxCh -> (all x (member(x,FUNS) ->
   equal(composite(x,composite(CHOICE,VERTSECT(inverse(x)))),id(R(x))))).
%  Theorem AC-FU-OO
AxCh -> (all x (FUNCTION(x) -> 
   ONEONE(composite(CHOICE,VERTSECT(inverse(x)))))).
%  Corollary AC-BIJ
AxCh -> (all x (member(x,FUNS) ->
   member(composite(CHOICE,VERTSECT(inverse(x))),BIJ))).
%  Theorem AC-FS-Q
AxCh -> (all x (member(x,FUNS) ->
   member(pair(D(x),R(x)),composite(Q,inverse(S))))).
%  Theorem AC-FU-Q
AxCh -> (all x (FUNCTION(x) ->
   subclass(composite(IMAGE(x),id(P(D(x)))),composite(Q,inverse(S))))).
%  Theorem AC-V
AxCh -> subclass(CHOICE,cart(V,V)).
%  Theorem AC-FP
AxCh -> equal(fix(composite(E,CHOICE)),complement(singleton(0))).
%  Theorem AC-MEM
AxCh -> (all x y (member(pair(x,y),CHOICE) -> member(y,x))).
%  Theorem AC-AP
AxCh -> (all x (member(x,V) -> (equal(0,x) | member(apply(CHOICE,x),x)))).
%  Lemma AC-SS-1
AxCh -> (all x (member(x,V) -> member(singleton(x),D(CHOICE)))).
%  Theorem AC-SS-2
AxCh -> (all x (member(x,V) -> member(pair(singleton(x),x),CHOICE))).
%  Lemma AC-Z-LEM
AxCh -> (all x y (member(x,y) ->
        (equal(x,0) | member(apply(CHOICE,x),image(CHOICE,y))))).
%  Theorem AC-Z
AxCh -> (all x y ((member(x,y) & subclass(cart(y,y),union(Id,DISJOINT)))
     -> (equal(x,0) | equal(intersection(x,image(CHOICE,y)),singleton(apply(CHOICE,x)))))).
%  Corollary AC-Z-COR
AxCh -> (all x (subclass(cart(x,x),union(Id,DISJOINT)) ->
        (member(0,x) | subclass(image(IMAGE(id(image(CHOICE,x))),x),R(SINGLETON))))).
%  Theorem AC-SG-1
AxCh -> subclass(inverse(SINGLETON),CHOICE).
%  Theorem AC-RA
AxCh -> equal(R(CHOICE),V).
%  Theorem AC-SG-2
AxCh -> equal(composite(CHOICE,SINGLETON),Id).
end_of_list.

list(demodulators).
equal(intersection(x,y),intersection(y,x)).                      % I-2
equal(union(x,y),union(y,x)).                                    % U-2
equal(U(P(x)),x).                                                % PC-7-COR
end_of_list.