% problem-set/analysis/limits/axioms.clauses
% created : 07/21/86                          
% revised : 07/20/88                          

%   Axioms of limit theorems                      
%
% declare_predicates(2,[EQUAL,LT]).
% declare_functions(2,[sum,f1]).
% declare_functions(1,[h,fp31,minus,f,fp32,g,fp33,abs]).
% declare_constants([0,a,l1,l2,b]).
% declare_variables([x,y,z,xa]).


% the less than operation is transitive 

-LT(x,y)  | -LT(y,z)  |  LT(x,z).

% axiom 1 

EQUAL(sum(x,0),x).
EQUAL(sum(0,x),x).
-LT(x,x).

% axiom 2 

-LT(0,x) | -LT(0,y) |  LT(0,f1(x,y)).
-LT(0,x) | -LT(0,y) |  LT(f1(x,y),x).
-LT(0,x) | -LT(0,y) |  LT(f1(x,y),y).

% axiom 3 

-LT(x,h(xa))  | -LT(y,h(xa))  |  LT(sum(x,y),xa).

% axiom 4 

-LT(sum(abs(x),abs(y)),xa)  |  LT(abs(sum(x,y)),xa).

% axiom 5 

EQUAL(sum(sum(x,y),z),sum(x,sum(y,z))).

% axiom 6 

EQUAL(sum(x,y),sum(y,x)).

% axiom 7 

-LT(0,xa)    |  LT(0,h(xa)).

% axiom 8 

EQUAL(minus(sum(x,y)),sum(minus(x),minus(y))).

% equality substitution axioms 

-EQUAL(x,y)  | -LT(x,z)  |  LT(y,z).
-EQUAL(x,y)  | -LT(z,x)  |  LT(z,y).
-EQUAL(x,y)  |  EQUAL(abs(x),abs(y)).
-EQUAL(x,y)  |  EQUAL(sum(x,z),sum(y,z)).
-EQUAL(x,y)  |  EQUAL(sum(z,x),sum(z,y)).
-EQUAL(x,y)  |  EQUAL(minus(x),minus(y)).
-EQUAL(x,y)  |  EQUAL(h(x),h(y)).
-EQUAL(x,y)  |  EQUAL(f(x),f(y)).
-EQUAL(x,y)  |  EQUAL(g(x),g(y)).
-EQUAL(x,y)  |  EQUAL(fp31(x),fp31(y)).
-EQUAL(x,y)  |  EQUAL(fp32(x),fp32(y)).
-EQUAL(x,y)  |  EQUAL(fp33(x),fp33(y)).
-EQUAL(x,y)  |  EQUAL(f1(x,z),f1(y,z)).
-EQUAL(x,y)  |  EQUAL(f1(z,x),f1(z,y)).
	
% equality axioms 

EQUAL(x,x).
-EQUAL(x,y)  |  EQUAL(y,x).
-EQUAL(x,y)  | -EQUAL(y,z)  |  EQUAL(x,z).