% problem-set/analysis/limits/prob1.ver2.in % created : 07/21/86 % revised : 07/20/88 % description : % % Problem contributed through private correspondance with W.W. Bledsoe. % representation : % % declare_predicates(2,[EQUAL,LT]). % declare_functions(2,[sum,f1]). % declare_functions(1,[h,fp31,minus,f,fp32,g,fp33,abs]). % declare_constants([0,a,l1,l2,b]). % declare_variables([x,y,z,xa]). % % No interpretations are available at this time. set(UR_res). assign(max_kept,1000). list(axioms). % axiom 1 EQUAL(sum(x,0),x). EQUAL(sum(0,x),x). -LT(x,x). % LT transitivity -LT(x,y) | -LT(y,z) | LT(x,z). % axiom 2 -LT(0,x) | -LT(0,y) | LT(0,f1(x,y)). -LT(0,x) | -LT(0,y) | LT(f1(x,y),x). -LT(0,x) | -LT(0,y) | LT(f1(x,y),y). % axiom 3 -LT(x,h(xa)) | -LT(y,h(xa)) | LT(sum(x,y),xa). % axiom 7 -LT(0,xa) | LT(0,h(xa)). end_of_list. list(sos). % denial of the theorem -LT(0,x) | LT(0,fp31(x)). -LT(0,x) | -LT(abs(sum(y,minus(a))),fp31(x)) | LT(abs(sum(f(y),minus(l1))),x). -LT(0,x) | LT(0,fp32(x)). -LT(0,x) | -LT(abs(sum(y,minus(a))),fp32(x)) | LT(abs(sum(g(y),minus(l2))),x). LT(0,b). -LT(0,x) | LT(abs(sum(fp33(x),minus(a))),x). -LT(0,x) | -LT(sum(abs(sum(f(fp33(x)),minus(l1))), abs(sum(g(fp33(x)),minus(l2)))),b). % equality substitution axioms -EQUAL(x,y) | -LT(x,z) | LT(y,z). -EQUAL(x,y) | -LT(z,x) | LT(z,y). -EQUAL(x,y) | EQUAL(abs(x),abs(y)). -EQUAL(x,y) | EQUAL(sum(x,z),sum(y,z)). -EQUAL(x,y) | EQUAL(sum(z,x),sum(z,y)). -EQUAL(x,y) | EQUAL(minus(x),minus(y)). -EQUAL(x,y) | EQUAL(h(x),h(y)). -EQUAL(x,y) | EQUAL(f(x),f(y)). -EQUAL(x,y) | EQUAL(g(x),g(y)). -EQUAL(x,y) | EQUAL(fp31(x),fp31(y)). -EQUAL(x,y) | EQUAL(fp32(x),fp32(y)). -EQUAL(x,y) | EQUAL(fp33(x),fp33(y)). -EQUAL(x,y) | EQUAL(f1(x,z),f1(y,z)). -EQUAL(x,y) | EQUAL(f1(z,x),f1(z,y)). % equality axioms EQUAL(x,x). -EQUAL(x,y) | EQUAL(y,x). -EQUAL(x,y) | -EQUAL(y,z) | EQUAL(x,z). % axiom 5 EQUAL(sum(sum(x,y),z),sum(x,sum(y,z))). % axiom 6 EQUAL(sum(x,y),sum(y,x)). % axiom 7 -LT(0,xa) | LT(0,h(xa)). % axiom 8 EQUAL(minus(sum(x,y)),sum(minus(x),minus(y))). end_of_list.