% problem-set/algebra/henkin.models/hp7.ver2.in
% 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                                    


set(ur_res).
set(para_into).
set(para_from_left).
set(para_from_right).
set(order_eq).
set(dynamic_demod).


list(axioms).

% 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) = x).

% HP 5:
-LE(x,y) | -LE(y,z) | LE(x,z).

% HP 6:
-LE(f(x,y),z) | LE(f(x,z),y).

end_of_list.


list(sos).

% denial of the theorem
LE(a,b).
-LE(f(c,b),f(c,a)).

end_of_list.


list(demodulators).

(f(x,1) = 0).
(f(0,x) = 0).
(f(x,x) = 0).
(f(x,0) = x).

end_of_list.
