% problem-set/algebra/henkin.models/hp8.ver3.clauses
% 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                                    


% 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   

% denial of the theorem
(f(a,b) = 0).
(f(f(a,c),f(b,c)) != 0).