% problem-set/algebra/henkin.models/hp7.ver2.clauses % created : 07/21/86 % revised : 07/18/89 % description: % % Theorem HP7: If x <= y, then z/y <= z/x. % representation: % % 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 % Equality axiom (x = x). % A0: definition of LE (less than or equal to ) -LE(x,y) | (f(x,y) = 0). (f(x,y) != 0) | LE(x,y). % A1: x/y <= x LE(f(x,y),x). % A2: (x/z) / (y/z) <= (x/y) / z LE(f(f(x,z),f(y,z)),f(f(x,y),z)). % 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 ) LE(x,1). % Implicit in equality formulation: '/' is well defined % HP 1: (f(x,1) = 0). % HP 2: (f(0,x) = 0). % HP 3: (f(x,x) = 0). % HP 4: (f(x,0) = 0). % HP 5: -LE(x,y) | -LE(y,z) | LE(x,z). % HP 6: -LE(f(x,y),z) | LE(f(x,z),y). % denial of the theorem LE(a,b). -LE(f(c,b),f(c,a)).