----- SUMMARY FOR THEOREM AC-FP IN DIRECTORY Q:\choice -----

% AC-FP.IN                 2000 February 12
% An immediate consequence of the axiom of choice.

formula_list(sos).
% negation of Theorem AC-FP
-(AxCh -> equal(fix(composite(E,CHOICE)),complement(singleton(0)))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Sun Feb 13 08:19:07 2000

Length of proof is 9. Level of proof is 3.

---------------- PROOF ----------------

5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y).
70 [] -AxCh | subclass(CHOICE,inverse(E)).
71 [] -AxCh | equal(D(CHOICE),complement(singleton(0))).
77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z).
421 [] -subclass(x,cart(V,V)) | -subclass(inverse(x),inverse(y))
           | subclass(x,y).
741 [] -subclass(x,y) | subclass(composite(z,x),composite(z,y)).
753 [] subclass(D(composite(x,y)),D(y)).
1144 [] subclass(id(x),cart(V,V)).
1165 [] subclass(fix(x),D(x)).
1186 [] -subclass(id(x),y) | subclass(x,fix(y)).
1210 [] subclass(id(D(x)),composite(inverse(x),x)).
1216 [] AxCh.
1217 [] -equal(fix(composite(E,CHOICE)),complement(singleton(0))).
1428 [] equal(inverse(composite(x,y)),composite(inverse(y),
          inverse(x))).
1570 [] equal(inverse(id(x)),id(x)).
1593 [binary,1216.1,71.1] equal(D(CHOICE),complement(singleton(0))).
1595 [binary,1216.1,70.1] subclass(CHOICE,inverse(E)).
1597 [binary,1217.1,5.3] 
          -subclass(fix(composite(E,CHOICE)),complement(singleton(0)))
           | -subclass(complement(singleton(0)),
          fix(composite(E,CHOICE))).
1598 [para_from,1593.1.1,1210.1.1.1] 
          subclass(id(complement(singleton(0))),
          composite(inverse(CHOICE),CHOICE)).
1602 [para_from,1593.1.1,753.1.2] 
          subclass(D(composite(x,CHOICE)),complement(singleton(0))).
1605 [binary,1595.1,741.1] 
          subclass(composite(x,CHOICE),composite(x,inverse(E))).
1615 [binary,1597.2,1186.2] 
          -subclass(fix(composite(E,CHOICE)),complement(singleton(0)))
           | -subclass(id(complement(singleton(0))),
          composite(E,CHOICE)).
1634 [ur,1602,77,1165] 
          subclass(fix(composite(x,CHOICE)),
          complement(singleton(0))).
1639 [ur,1605,77,1598] 
          subclass(id(complement(singleton(0))),
          composite(inverse(CHOICE),inverse(E))).
1660 [binary,1615.2,421.3,demod,1570,1428,unit_del,1634,1144,1639] 
          $F.

------------ end of proof -------------

clauses generated   11184
Kbytes malloced      1309
user CPU time           1.75  seconds