----- SUMMARY FOR THEOREM FS-NEST IN DIRECTORY Q:\fs ----- % FS-NEST.IN 1997 August 24 % Union of a nest of functions formula_list(sos). % negation of Theorem FS-NEST -(all x ((subclass(x,FUNS) & subclass(cart(x,x),union(S,inverse(S)))) -> FUNCTION(U(x)))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Sun Aug 24 18:40:45 1997 Length of proof is 35. Level of proof is 21. ---------------- PROOF ---------------- 1 [] -subclass(x,y) | -member(u,x) | member(u,y). 15 [] -member(pair(u,v),cart(x,y)) | member(v,y). 16 [] member(pair(u,v),cart(x,y)) | -member(u,x) | -member(v,y). 17 [] -member(z,cart(x,y)) | equal(z,pair(first(z),second(z))). 26 [] -member(z,complement(x)) | -member(z,x). 64 [] FUNCTION(xf) | -subclass(xf,cart(V,V)) | -SINGLEVALUED(xf). 171 [] -member(x,union(y,z)) | member(x,y) | member(x,z). 207 [] subclass(cart(x,y),cart(V,V)). 254 [] -disjoint(x,y) | subclass(x,complement(y)). 263 [] member(notsub(x,complement(y)),x) | disjoint(x,y). 264 [] member(notsub(x,complement(y)),y) | disjoint(x,y). 271 [] -member(pair(x,y),xr) | -member(pair(x,y),cart(V,V)) | member(x,D(xr)). 305 [] -member(pair(u,v),inverse(x)) | member(pair(v,u),x). 372 [] -member(x,U(y)) | member(x,ran(E,x,y)). 373 [] -member(x,U(y)) | member(ran(E,x,y),y). 375 [] -subclass(x,y) | subclass(U(x),U(y)). 522 [] -member(pair(x,y),S) | subclass(x,y). 744 [] subclass(cross(x,y),cart(cart(V,V),cart(V,V))). 772 [] -disjoint(cart(x,x),cross(Id,complement(Id))) | SINGLEVALUED(x). 782 [] -member(x,FUNS) | disjoint(cart(x,x), cross(Id,complement(Id))). 790 [] subclass($c1,FUNS). 791 [] subclass(cart($c1,$c1),union(S,inverse(S))). 792 [] -FUNCTION(U($c1)). 841 [] equal(D(cart(x,x)),x). 945 [] equal(U(FUNS),cart(V,V)). 947 [] equal(notsub(cart(U(x),U(x)),complement(cross(Id,complement(Id)))), n$(x)). 948 [] equal(first(n$(x)),p$(x)). 949 [] equal(second(n$(x)),q$(x)). 950 [] equal(ran(E,p$(x),x),f$(x)). 951 [] equal(ran(E,q$(x),x),g$(x)). 953 [ur,790,375,demod,945] subclass(U($c1),cart(V,V)). 959 [ur,953,64,792] -SINGLEVALUED(U($c1)). 960 [ur,959,772] -disjoint(cart(U($c1),U($c1)), cross(Id,complement(Id))). 965 [ur,960,264,demod,947] member(n$($c1),cross(Id,complement(Id))). 966 [ur,960,263,demod,947] member(n$($c1),cart(U($c1),U($c1))). 968 [ur,965,26] -member(n$($c1),complement(cross(Id, complement(Id)))). 969 [ur,965,1,744] member(n$($c1),cart(cart(V,V),cart(V,V))). 973,972 [ur,969,17,demod,948,949] equal(n$($c1),pair(p$($c1),q$($c1))). 974 [ur,969,1,207,demod,973] member(pair(p$($c1),q$($c1)),cart(V,V)). 976 [back_demod,968,demod,973] -member(pair(p$($c1),q$($c1)),complement(cross(Id, complement(Id)))). 977 [back_demod,966,demod,973] member(pair(p$($c1),q$($c1)),cart(U($c1),U($c1))). 982 [ur,977,271,974,demod,841] member(p$($c1),U($c1)). 983 [ur,977,15] member(q$($c1),U($c1)). 985 [ur,982,373,demod,950] member(f$($c1),$c1). 986 [ur,982,372,demod,950] member(p$($c1),f$($c1)). 988 [ur,985,1,790] member(f$($c1),FUNS). 998 [ur,988,782] disjoint(cart(f$($c1),f$($c1)), cross(Id,complement(Id))). 1002 [ur,983,373,demod,951] member(g$($c1),$c1). 1003 [ur,983,372,demod,951] member(q$($c1),g$($c1)). 1008 [ur,1002,16,985] member(pair(f$($c1),g$($c1)),cart($c1,$c1)). 1011 [ur,1002,1,790] member(g$($c1),FUNS). 1025 [ur,1011,782] disjoint(cart(g$($c1),g$($c1)), cross(Id,complement(Id))). 1040 [ur,998,254] subclass(cart(f$($c1),f$($c1)), complement(cross(Id,complement(Id)))). 1042 [ur,1008,1,791] member(pair(f$($c1),g$($c1)), union(S,inverse(S))). 1046 [ur,1025,254] subclass(cart(g$($c1),g$($c1)), complement(cross(Id,complement(Id)))). 1055 [ur,1040,1,976] -member(pair(p$($c1),q$($c1)), cart(f$($c1),f$($c1))). 1060 [ur,1046,1,976] -member(pair(p$($c1),q$($c1)), cart(g$($c1),g$($c1))). 1076 [ur,1055,16,986] -member(q$($c1),f$($c1)). 1077 [ur,1076,1,1003] -subclass(g$($c1),f$($c1)). 1078 [ur,1077,522] -member(pair(g$($c1),f$($c1)),S). 1081 [ur,1078,305] -member(pair(f$($c1),g$($c1)),inverse(S)). 1088 [ur,1081,171,1042] member(pair(f$($c1),g$($c1)),S). 1096 [ur,1088,522] subclass(f$($c1),g$($c1)). 1110 [ur,1096,1,986] member(p$($c1),g$($c1)). 1111 [ur,1110,16,1003] member(pair(p$($c1),q$($c1)),cart(g$($c1),g$($c1))). 1112 [binary,1111.1,1060.1] $F. ------------ end of proof ------------- clauses generated 20677 Kbytes malloced 830 user CPU time 7.09 seconds