% problem-set/algebra/henkin.models/hp11.ver1.in
% created : 07/21/86
% revised : 07/18/89

% description:
%
% Theorem HP11: If & is defined on the set of all z' (z'=1/z) by 
% x' & y' = x'/(1/y'), then & is commutative.

% 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,q,r).
%
% 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_seconds,3600).
assign(max_mem,2000).
set(unit_deletion).
set(factor).


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).
(f(x,1) = 0).

% HP 2:
P(0,x,0).
(f(0,x) = 0).

% HP 3:
P(x,x,0).
(f(x,x) = 0).

% HP 4:
P(x,0,x).
(f(x,0) = x).

% HP 5:
-LE(x,y) | -LE(y,z) | LE(x,z).
(f(x,y) != 0) | (f(y,z) != 0) | (f(x,z) = 0).

% HP 6:
-P(x,y,z) | -LE(z,w) | -P(x,w,v) | LE(v,y).
-LE(f(x,y),w) | LE(f(x,w),y).
(f(f(x,y),w) != 0) | (f(f(x,w),y) = 0).

% HP 7:
-LE(x,y) | -P(z,y,w) | -P(z,x,v) | LE(w,v).
-LE(x,y) | LE(f(z,y),f(z,x)).
(f(x,y) != 0) | (f(f(z,y),f(z,x)) = 0).

% HP 8:
-LE(x,y) | -P(x,z,w) | -P(y,z,v) | LE(w,v).
-LE(x,y) | LE(f(x,z),f(y,z)).
(f(x,y) != 0) | (f(f(x,z),f(y,z)) = 0).

% HP 9:
-P(1,x,y) | -P(1,y,z) | -P(1,z,w) | (y = w).
(f(1,f(1,f(1,x))) = f(1,x)).

% HP 10:
-P(1,x,y) | -P(1,y,z) | -P(y,z,w) | (y = w).
(f(f(1,x),f(1,f(1,x))) = f(1,x)).

% additional
LE(x,x).

end_of_list.


list(sos).

% denial of the theorem
P(1,a,c).
P(1,b,d).
P(1,d,e).
P(c,e,p).
P(1,c,q).
P(d,q,r).
(p != r).

end_of_list.


list(demodulators).

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

end_of_list.


weight_list(pick_and_purge).

weight(x, 10).
weight(f(1,1), 5).
weight(0, -1).
weight(1, -1).

end_of_list.
