----- SUMMARY FOR THEOREM DK-C-OM IN DIRECTORY Q:\dedekind ----- % DK-C-OM.IN 2000 June 12 % omega is not Dedekind finite. formula_list(sos). % negation of Theorem DK-C-OM member(omega,DEDEKIND). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Mon Jun 12 09:04:15 2000 Length of proof is 16. Level of proof is 9. ---------------- PROOF ---------------- 14 [] member(pair(u,v),cart(x,y)) | -member(u,x) | -member(v,y). 22 [] -member(x,complement(y)) | -member(x,y). 53 [] member(omega,V). 77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z). 90 [] member(0,V). 93 [] subclass(intersection(x,y),x). 136 [] -subclass(complement(x),complement(y)) | subclass(y,x). 138 [] -equal(intersection(x,y),x) | subclass(x,y). 157 [] -subclass(x,y) | -subclass(intersection(complement(x),z),y) | subclass(z,y). 246 [] -member(x,V) | -subclass(singleton(x),y) | member(x,y). 292 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)). 373 [] -member(pair(x,y),z) | -subclass(z,cart(V,V)) | member(x,D(z)). 753 [] -member(pair(x,y),z) | -member(pair(x,y),cart(V,V)) | -member(pair(y,u),v) | -member(pair(y,u),cart(V,V)) | member(pair(x,u),composite(v,z)). 1175 [] -member(x,V) | -member(pair(x,x),y) | member(x,fix(y)). 1459 [] -EQUIVALENCE(x) | -member(pair(y,z),x) | member(pair(z,y),x). 1475 [] EQUIVALENCE(cart(x,x)). 1611 [] -member(0,pair(x,y)) | -member(pair(x,y),cart(V,V)). 1672 [] subclass(PS,cart(V,V)). 1677 [] -member(x,V) | -subclass(y,x) | equal(y,x) | member(pair(y,x),PS). 2718 [] equal(composite(PS,Q),composite(Q,PS)). 2894 [] subclass(singleton(0),omega). 2918 [] member(pair(omega,intersection(omega,complement(singleton(0)))), Q). 3303 [] equal(complement(fix(composite(Q,PS))),DEDEKIND). 3304 [] member(omega,DEDEKIND). 3336 [] equal(complement(complement(x)),x). 3801 [] equal(D(PS),V). 4344 [ur,3304,292,3304] member(pair(omega,omega),cart(V,V)). 4345 [para_into,3304.1.2,3303.1.2] member(omega,complement(fix(composite(Q,PS)))). 4346 [binary,4344.1,1611.2] -member(0,pair(omega,omega)). 4349 [binary,4345.1,22.2,demod,3336] -member(omega,fix(composite(Q,PS))). 4353 [binary,4346.1,246.3,unit_del,90] -subclass(singleton(0),pair(omega,omega)). 4362 [binary,4349.1,1175.3,unit_del,53] -member(pair(omega,omega),composite(Q,PS)). 4374 [binary,4353.1,136.2] -subclass(complement(pair(omega,omega)), complement(singleton(0))). 4395 [para_into,4362.1.2,2718.1.2] -member(pair(omega,omega),composite(PS,Q)). 4410 [ur,4374,157,93] -subclass(singleton(0),complement(singleton(0))). 4446 [binary,4395.1,753.5] -member(pair(omega,x),Q) | -member(pair(omega,x),cart(V,V)) | -member(pair(x,omega),PS) | -member(pair(x,omega), cart(V,V)). 4472 [ur,4410,77,2894] -subclass(omega,complement(singleton(0))). 4542 [binary,4446.1,2918.1] -member(pair(omega,intersection(omega,complement(singleton(0)))), cart(V,V)) | -member(pair(intersection(omega, complement(singleton(0))),omega),PS) | -member(pair(intersection(omega,complement(singleton(0))), omega),cart(V,V)). 4583 [binary,4472.1,138.2] -equal(intersection(omega,complement(singleton(0))),omega). 4651 [binary,4542.1,1459.3,unit_del,1475,factor_simp] -member(pair(intersection(omega,complement(singleton(0))), omega),PS) | -member(pair(intersection(omega, complement(singleton(0))),omega),cart(V,V)). 4676 [binary,4583.1,1677.3,unit_del,53,93] member(pair(intersection(omega,complement(singleton(0))), omega),PS). 4737 [binary,4651.2,14.1,unit_del,4676,53] -member(intersection(omega,complement(singleton(0))),V). 4760 [binary,4676.1,373.1,demod,3801,unit_del,1672,4737] $F. ------------ end of proof ------------- clauses generated 171977 Kbytes malloced 3161 user CPU time 32.79 seconds