----- SUMMARY FOR THEOREM AC-VS-DO IN DIRECTORY Q:\choice -----

% AC-VS-DO.IN                 2000 June 5

formula_list(sos).
% negation of Theorem AC-VS-DO
-(AxCh -> (all x equal(D(composite(CHOICE,VERTSECT(x))),
           intersection(D(x),D(VERTSECT(x)))))).
end_of_list.


----- Otter 3.0.4, August 1995 -----
The job was started by ??? on ???, Mon Jun 05 21:56:16 2000

Length of proof is 2. Level of proof is 2.

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

71 [] -AxCh | equal(D(CHOICE),complement(singleton(0))).
78 [] equal(x,x).
778 [] equal(D(composite(x,y)),image(inverse(y),D(x))).
2079 [] AxCh.
2080 [] -equal(D(composite(CHOICE,VERTSECT($c1))),
          intersection(D($c1),D(VERTSECT($c1)))).
2741 [] equal(image(inverse(VERTSECT(x)),complement(singleton(0))),
          intersection(D(x),D(VERTSECT(x)))).
2751,2750 [ur,2079,71] equal(D(CHOICE),complement(singleton(0))).
2752 [para_into,2080.1.1,778.1.1,demod,2751,2741] 
          -equal(intersection(D($c1),D(VERTSECT($c1))),
          intersection(D($c1),D(VERTSECT($c1)))).
2753 [binary,2752.1,78.1] $F.

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

clauses generated      44
Kbytes malloced      1979
user CPU time           1.60  seconds