----- SUMMARY FOR THEOREM GT-SR-2 IN DIRECTORY Q:\greatest ----- % GT-SR-2.IN 2000 December 20 % This was first derived using the GOEDEL program. Theorem GT-UB-U % proved to be a crucial lemma in obtaining this proof. formula_list(sos). % negation of Theorem GT-SR-2 -(all x equal(composite(GREATEST(x),S),composite(id(fix(x)),UB(x)))). end_of_list. ----- Otter 3.0.4, August 1995 ----- The job was started by ??? on ???, Wed Dec 20 14:38:07 2000 Length of proof is 17. Level of proof is 9. ---------------- PROOF ---------------- 1 [] -member(x,y) | -subclass(y,z) | member(x,z). 2 [] member(notsub(x,y),x) | subclass(x,y). 3 [] -member(notsub(x,y),y) | subclass(x,y). 5 [] -subclass(x,y) | -subclass(y,x) | equal(x,y). 15 [] -member(x,cart(y,z)) | equal(pair(first(x),second(x)),x). 76 [] subclass(x,x). 144 [] subclass(x,union(x,y)). 379 [] -member(pair(x,y),z) | -subclass(z,cart(V,V)) | member(x,D(z)). 751 [] subclass(composite(x,y),cart(V,V)). 773 [] -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)). 1225 [] subclass(composite(id(x),y),y). 1268 [] -member(pair(x,y),composite(id(z),u)) | member(y,z). 1393 [] -member(x,V) | -subclass(y,x) | member(pair(y,x),S). 1434 [] -member(union(x,y),V) | member(pair(x,y),cart(V,V)). 1478 [] subclass(GREATEST(x),cart(V,V)). 1489 [] -member(pair(x,y),UB(z)) | -member(pair(u,y),GREATEST(z)) | member(pair(union(x,u),y),GREATEST(z)). 1491 [] -member(x,fix(y)) | member(pair(singleton(x),x),GREATEST(y)). 1492 [] subclass(composite(GREATEST(x),S),composite(id(fix(x)), UB(x))). 1493 [] -equal(composite(GREATEST($c1),S),composite(id(fix($c1)), UB($c1))). 1541 [] equal(union(x,union(x,y)),union(x,y)). 1581 [] equal(D(cart(x,x)),x). 1927 [] equal(notsub(composite(id(fix(x)),UB(x)), composite(GREATEST(x),S)),n$(x)). 1928 [] equal(first(n$(x)),f$(x)). 1929 [] equal(second(n$(x)),s$(x)). 1930 [binary,1493.1,5.3,unit_del,1492] -subclass(composite(id(fix($c1)), UB($c1)),composite(GREATEST($c1),S)). 1931 [binary,1930.1,3.2,demod,1927] -member(n$($c1),composite(GREATEST($c1),S)). 1932 [binary,1930.1,2.2,demod,1927] member(n$($c1),composite(id(fix($c1)),UB($c1))). 1935 [ur,1932,1,1225] member(n$($c1),UB($c1)). 1936 [ur,1932,1,751] member(n$($c1),cart(V,V)). 1943,1942 [binary,1936.1,15.1,demod,1928,1929,flip.1] equal(n$($c1),pair(f$($c1),s$($c1))). 1947 [back_demod,1935,demod,1943] member(pair(f$($c1),s$($c1)),UB($c1)). 1950 [back_demod,1932,demod,1943] member(pair(f$($c1),s$($c1)),composite(id(fix($c1)), UB($c1))). 1951 [back_demod,1931,demod,1943] -member(pair(f$($c1),s$($c1)),composite(GREATEST($c1),S)). 1966 [binary,1947.1,1489.1] -member(pair(x,s$($c1)),GREATEST($c1)) | member(pair(union(f$($c1),x),s$($c1)),GREATEST($c1)). 1970 [binary,1950.1,1268.1] member(s$($c1),fix($c1)). 1971 [binary,1951.1,773.5] -member(pair(f$($c1),x),S) | -member(pair(f$($c1), x),cart(V,V)) | -member(pair(x,s$($c1)),GREATEST($c1)) | -member(pair(x,s$($c1)),cart(V,V)). 1988 [binary,1966.1,1491.2,unit_del,1970] member(pair(union(f$($c1),singleton(s$($c1))), s$($c1)),GREATEST($c1)). 2009 [binary,1971.2,1434.2] -member(pair(f$($c1),x),S) | -member(pair(x,s$($c1)), GREATEST($c1)) | -member(pair(x,s$($c1)),cart(V,V)) | -member(union(f$($c1),x),V). 2059 [ur,1988,1,1478] member(pair(union(f$($c1),singleton(s$($c1))), s$($c1)),cart(V,V)). 2158 [binary,2009.2,1988.1,demod,1541,unit_del,2059] -member(pair(f$($c1),union(f$($c1),singleton(s$($c1)))),S) | -member(union(f$($c1),singleton(s$($c1))),V). 2323 [binary,2059.1,379.1,demod,1581,unit_del,76] member(union(f$($c1),singleton(s$($c1))),V). 2654 [binary,2158.1,1393.3,unit_del,2323,2323,144] $F. ------------ end of proof ------------- clauses generated 60424 Kbytes malloced 1947 user CPU time 15.21 seconds