----- SUMMARY FOR THEOREM DIF-AP1 IN DIRECTORY Q:\dif ----- % DIF-AP1.IN 2000 August 16 formula_list(sos). % negation of Theorem DIF-AP1 -(all x (member(x,cart(V,V)) -> equal(apply(DIF,x), intersection(first(x),complement(second(x)))))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Wed Aug 16 23:51:46 2000 Length of proof is 20. Level of proof is 5. ---------------- PROOF ---------------- 78 [] equal(x,x). 93 [] subclass(intersection(x,y),x). 251 [] member(singleton(x),pair(x,y)). 262 [] -member(x,V) | -member(y,pair(x,z)) | member(x,y). 270 [] -member(pair(x,y),cart(V,V)) | equal(second(pair(x,y)),y). 293 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)). 385 [] -member(x,y) | -member(x,cart(V,V)) | member(first(x),D(y)). 408 [] -member(x,cart(V,V)) | equal(D(singleton(x)), singleton(first(x))). 467 [] -member(x,cart(V,V)) | equal(R(singleton(x)), singleton(second(x))). 551 [] equal(image(V,R(x)),image(V,D(x))). 552 [] -member(x,V) | equal(image(V,singleton(x)),V). 596 [] -member(x,V) | equal(U(singleton(x)),x). 603 [] -member(x,cart(V,V)) | equal(U(R(singleton(x))),second(x)). 638 [] -member(x,cart(V,V)) | equal(A(x),singleton(first(x))). 639 [] -member(x,cart(V,V)) | equal(A(A(x)),first(x)). 663 [] -member(x,cart(y,z)) | member(x,P(P(union(y,P(z))))). 1192 [] FUNCTION(id(x)). 1346 [] -member(x,y) | -subclass(z,x) | member(z,image(inverse(S), y)). 1822 [] -FUNCTION(x) | -member(pair(y,z),x) | equal(apply(x,y),z). 1823 [] -member(x,y) | equal(apply(id(y),x),x). 1854 [] -FUNCTION(composite(Id,x)) | -member(y,D(x)) | equal(apply(composite(z,x),y),apply(z,apply(x,y))). 2073 [] -equal(image(x,singleton(first(y))),second(y)) | -member(y,cart(V,V)) | member(y,VERTSECT(x)). 2086 [] FUNCTION(VERTSECT(x)). 2438 [] equal(composite(VERTSECT(intersection(composite(inverse(E), FIRST),composite(complement(inverse(E)),SECOND))), id(cart(V,V))),DIF). 2440 [] member($c1,cart(V,V)). 2441 [] -equal(apply(DIF,$c1),intersection(first($c1), complement(second($c1)))). 2468 [] equal(intersection(V,x),x). 2476 [] equal(complement(V),0). 2483 [] equal(union(x,0),x). 2486 [] equal(union(x,x),x). 2528 [] equal(D(cart(x,x)),x). 2543 [] equal(R(inverse(x)),D(x)). 2558 [] equal(image(x,V),R(x)). 2564 [] equal(image(intersection(x,y),singleton(z)), intersection(image(x,singleton(z)),image(y,singleton(z)))). 2587 [] equal(image(complement(x),singleton(y)), intersection(image(V,singleton(y)), complement(image(x,singleton(y))))). 2590 [] equal(image(inverse(E),x),U(x)). 2607 [] equal(A(singleton(x)),union(x,complement(image(V, singleton(x))))). 2609 [] equal(A(pair(x,y)),singleton(x)). 2613 [] equal(P(V),V). 2662 [] equal(image(composite(x,y),z),image(x,image(y,z))). 2679 [] equal(D(S),V). 2793 [] equal(composite(Id,id(x)),id(x)). 2809 [] equal(D(id(x)),x). 3136 [] equal(image(FIRST,x),D(x)). 3161 [] equal(image(SECOND,x),R(x)). 3270,3269 [ur,2440,1823] equal(apply(id(cart(V,V)),$c1),$c1). 3271 [ur,2440,663,demod,2613,2486,2613,2613] member($c1,V). 3273,3272 [ur,2440,638] equal(A($c1),singleton(first($c1))). 3275,3274 [ur,2440,467] equal(R(singleton($c1)),singleton(second($c1))). 3278,3277 [ur,2440,408] equal(D(singleton($c1)),singleton(first($c1))). 3279 [ur,2440,385,2440,demod,2528] member(first($c1),V). 3280 [para_into,2441.1.1.1,2438.1.2] -equal(apply(composite(VERTSECT(intersection(composite(inver se(E),FIRST),composite(complement(inverse(E)),SECOND))), id(cart(V,V))),$c1),intersection(first($c1), complement(second($c1)))). 3286,3285 [ur,3271,552] equal(image(V,singleton($c1)),V). 3287 [ur,3271,262,251] member($c1,singleton($c1)). 3293,3292 [para_from,3272.1.2,596.2.1.1,demod,3273,unit_del,3279] equal(U(singleton(first($c1))),first($c1)). 3295,3294 [para_from,3272.1.2,552.2.1.2,demod,3273,unit_del,3279] equal(image(V,singleton(first($c1))),V). 3302,3301 [para_from,3274.1.1,603.2.1.1,unit_del,2440] equal(U(singleton(second($c1))),second($c1)). 3304,3303 [para_from,3274.1.1,551.1.1.2,demod,3278,3295] equal(image(V,singleton(second($c1))),V). 3308 [ur,3279,1346,93,demod,2558,2543,2679] member(intersection(first($c1),x),V). 3309 [para_into,3280.1.1,1854.3.1,demod,3270, 2793,2809,unit_del,1192,2440] -equal(apply(VERTSECT(intersection(composite(inverse(E), FIRST),composite(complement(inverse(E)),SECOND))), $c1),intersection(first($c1),complement(second($c1)))). 3329 [ur,3308,293,3287] member(pair($c1,intersection(first($c1),x)),cart(V,V)). 3331 [ur,3309,1822,2086] -member(pair($c1,intersection(first($c1), complement(second($c1)))),VERTSECT(intersection(composite(in verse(E),FIRST),composite(complement(inverse(E)), SECOND)))). 3335,3334 [ur,3329,639,demod,2609,2607,3286,2476,2483,flip.1] equal(first(pair($c1,intersection(first($c1),x))),$c1). 3342,3341 [ur,3329,270] equal(second(pair($c1,intersection(first($c1),x))), intersection(first($c1),x)). 3345 [ur,3331,2073,3329,demod,3335,2564,2662, 3136,3278,2590,3293,2662,3161,3275, 2587,3304,2590,3302,2468,3342] -equal(intersection(first($c1),complement(second($c1))), intersection(first($c1),complement(second($c1)))). 3346 [binary,3345.1,78.1] $F. ------------ end of proof ------------- clauses generated 50645 Kbytes malloced 2458 user CPU time 7.08 seconds