----- SUMMARY FOR THEOREM FS-CUP IN DIRECTORY Q:\fs ----- % FS-CUP.IN 2000 March 9 % Reformulation of Theorem 3.12 in Hrbacek and Jech, page 26. formula_list(sos). % negation of Theorem FS-CUP -(all x (subclass(image(CUP,cart(x,x)),FUNS) -> FUNCTION(U(x)))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Thu Mar 09 16:47:37 2000 Length of proof is 19. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -member(x,y) | -subclass(y,z) | member(x,z). 14 [] member(pair(u,v),cart(x,y)) | -member(u,x) | -member(v,y). 77 [] -subclass(x,y) | -subclass(y,z) | subclass(x,z). 123 [] -member(x,y) | member(x,union(y,z)). 124 [] -member(x,y) | member(x,union(z,y)). 290 [] -member(u,x) | -member(v,y) | member(pair(u,v),cart(V,V)). 498 [] -member(x,y) | -member(pair(x,z),u) | -subclass(u,cart(V,V)) | member(z,image(u,y)). 580 [] -member(x,U(y)) | member(x,ran(E,x,y)). 581 [] -member(x,U(y)) | member(ran(E,x,y),y). 583 [] -subclass(x,y) | subclass(U(x),U(y)). 924 [] -subclass(x,cart(V,V)) | equal(composite(Id,x),x). 1085 [] member(pair(sv3(composite(x,y)),sv1(composite(x,y))), composite(x,y)) | FUNCTION(composite(x,y)). 1086 [] member(pair(sv3(composite(x,y)),sv2(composite(x,y))), composite(x,y)) | FUNCTION(composite(x,y)). 1087 [] -equal(sv2(composite(x,y)),sv1(composite(x,y))) | FUNCTION(composite(x,y)). 1097 [] -FUNCTION(x) | -member(pair(y,z),x) | -member(pair(y,u),x) | equal(z,u). 2241 [] subclass(CUP,cart(V,V)). 2247 [] -member(pair(x,y),cart(V,V)) | member(pair(pair(x,y),union(x,y)), CUP). 2248 [] subclass(x,image(CUP,cart(x,x))). 2281 [] -member(x,FUNS) | FUNCTION(x). 2286 [] subclass(image(CUP,cart($c1,$c1)),FUNS). 2287 [] -FUNCTION(U($c1)). 2334 [] equal(union(x,y),union(y,x)). 3062 [] equal(U(FUNS),cart(V,V)). 3063 [] equal(ran(E,pair(sv3(U(x)),sv1(U(x))),x),f1$(x)). 3064 [] equal(ran(E,pair(sv3(U(x)),sv2(U(x))),x),f2$(x)). 3066 [ur,2286,77,2248] subclass($c1,FUNS). 3070 [ur,3066,583,demod,3062] subclass(U($c1),cart(V,V)). 3075,3074 [ur,3070,924] equal(composite(Id,U($c1)),U($c1)). 3080 [para_from,3074.1.1,1087.2.1,demod,3075,3075,unit_del,2287] -equal(sv2(U($c1)),sv1(U($c1))). 3081 [para_from,3074.1.1,1086.2.1,demod,3075,3075,3075,unit_del,2287] member(pair(sv3(U($c1)),sv2(U($c1))),U($c1)). 3082 [para_from,3074.1.1,1085.2.1,demod,3075,3075,3075,unit_del,2287] member(pair(sv3(U($c1)),sv1(U($c1))),U($c1)). 3084 [ur,3081,581,demod,3064] member(f2$($c1),$c1). 3085 [ur,3081,580,demod,3064] member(pair(sv3(U($c1)),sv2(U($c1))),f2$($c1)). 3090 [ur,3082,581,demod,3063] member(f1$($c1),$c1). 3091 [ur,3082,580,demod,3063] member(pair(sv3(U($c1)),sv1(U($c1))),f1$($c1)). 3109 [ur,3085,123] member(pair(sv3(U($c1)),sv2(U($c1))), union(f2$($c1),x)). 3120 [ur,3090,290,3084] member(pair(f2$($c1),f1$($c1)),cart(V,V)). 3125 [ur,3090,14,3084] member(pair(f2$($c1),f1$($c1)),cart($c1,$c1)). 3129 [ur,3091,124] member(pair(sv3(U($c1)),sv1(U($c1))), union(x,f1$($c1))). 3159 [ur,3120,2247,demod,2334] member(pair(pair(f2$($c1),f1$($c1)),union(f1$($c1),f2$($c1))), CUP). 3177 [ur,3129,1097,3109,3080,demod,2334] -FUNCTION(union(f1$($c1),f2$($c1))). 3203 [ur,3159,498,3125,2241] member(union(f1$($c1),f2$($c1)),image(CUP,cart($c1,$c1))). 3218 [ur,3177,2281] -member(union(f1$($c1),f2$($c1)),FUNS). 3240 [ur,3203,1,2286] member(union(f1$($c1),f2$($c1)),FUNS). 3241 [binary,3240.1,3218.1] $F. ------------ end of proof ------------- clauses generated 191714 Kbytes malloced 2331 user CPU time 29.66 seconds