% problem-set/algebra/henkin.models/hp10.ver1.in % created : 07/21/86 % revised : 07/18/89 % description: % % Theorem HP10: For x'=1/x, x' = x'/(1/x'). % representation: % % declare_predicate(3,P). % declare_predicates(2,[LE,=]). % declare_function(2,f). % declare_variables(x,y,z,u,v,w). % declare_constants(0,1,a,b,c,d,e). % % P(x,y,z) : means x/y = z % LE : means less than or equal % f(x,y) : denotes x/y set(hyper_res). set(ur_res). set(order_eq). set(dynamic_demod). assign(max_mem,1500). assign(max_seconds,1800). list(axioms). % A0: definition of less than or equal to -LE(x,y) | P(x,y,0). -P(x,y,0) | LE(x,y). % A1: x/y <= x -P(x,y,z) | LE(z,x). % A2: (x/z) / (y/z) <= (x/y) / z -P(x,y,v1) | -P(y,z,v2) | -P(x,z,v3) | -P(v3,v2,v4) | -P(v1,z,v5) | LE(v4,v5). % A3: 0 <= x LE(0,x). % A4: x <= y and y <= x implies that x = y -LE(x,y) | -LE(y,x) | (x = y). % A5: x <= 1 (Thus an implicative model with unit 1) LE(x,1). % closure of '/' P(x,y,f(x,y)). % '/' is well defined -P(x,y,z) | -P(x,y,w) | (z = w). % Equality axioms (x = x). (x != y) | (y = x). (x != y) | (y != z) | (x = z). % Equality substitution axioms (x != y) | -P(x,w,z) | P(y,w,z). (x != y) | -P(w,x,z) | P(w,y,z). (x != y) | -P(w,z,x) | P(w,z,y). (x != y) | -LE(x,z) | LE(y,z). (x != y) | -LE(z,x) | LE(z,y). (x != y) | (f(x,w) = f(y,w)). (x != y) | (f(w,x) = f(w,y)). % HP 1: P(x,1,0). % HP 2: P(0,x,0). % HP 3: P(x,x,0). % HP 4: P(x,0,x). % HP 5: -LE(x,y) | -LE(y,z) | LE(x,z). % HP 6: -P(x,y,z) | -LE(z,w) | -P(x,w,v) | LE(v,y). % HP 7: -LE(x,y) | -P(z,y,w) | -P(z,x,v) | LE(w,v). % HP 8: -LE(x,y) | LE(f(x,z),f(y,z)). end_of_list. list(sos). % denial of the theorem P(1,a,b). P(1,b,c). P(b,c,d). (b != d). end_of_list. list(demodulators). (f(x,1) = 0). (f(0,x) = 0). (f(x,x) = 0). (f(x,0) = x). end_of_list.