% problem-set/algebra/henkin.models/hp8.ver3.in % created : 07/19/89 % revised : 07/19/89 % description: % % Theorem HP8: If x <= y, then x/z <= y/z. % representation: % % declare_predicate(2,=). % declare_function(2,f). % declare_variables(x,y,z,u,v,w). % declare_constants(0,1,a,b,c,d,e). % % f(x,y) : denotes x/y set(para_from). set(para_from_left). set(para_from_right). set(order_eq). assign(max_seconds,1800). list(axioms). % Equality axiom (x = x). % A0: definition of LE (less than or equal to ) % Used to replace all further occurrences of LE(x,y) % -LE(x,y) | (f(x,y) = 0). % (f(x,y) != 0) | LE(x,y). % A1: x/y <= x (f(f(x,y),x) = 0). % A2: (x/z) / (y/z) <= (x/y) / z (f(f(f(x,z),f(y,z)),f(f(x,y),z)) = 0). % A3: 0<=x NOTE: this axiom is dependant (f(0,x) = 0). % A4: x <= y and y <= x implies that x = y (f(x,y) != 0) | (f(y,x) != 0) | (x = y). % A5: x <= 1 (Thus an implicative model with unit ) (f(x,1) = 0). % Implicit in equality formulation: '/' is well defined end_of_list. list(sos). % denial of the theorem (f(a,b) = 0). (f(f(a,c),f(b,c)) != 0). end_of_list. list(demodulators). (f(x,1) = 0). (f(0,x) = 0). (f(x,x) = 0). (f(x,0) = x). end_of_list.