/*

This system can be viewed as modelling rational unification
The variables in input equations are constants which may be equated
to any other term in the course of unification.

With the precedence-modified subterm order
we may use an auxiliary projection function
p to formalize injectivity of function symbols
even though input queries do not contain p.
We have inp(f(X))> s(f(X)) in the ordering.

Therefore we get complexity n log n.

*/


:-option(special_relations(off)).  

% equality
eq(X,X).
eq(X,Y) -> eq(Y,X).
eq(X,Y), eq(Y,Z) -> eq(X,Z).

eq(X,Y), eq(U,V), eq(f(X,U),Z) -> eq(f(Y,V),Z).

% injectivity

eq(f(X,Y),f(U,V)) -> eq(X,U).
eq(f(X,Y),f(U,V)) -> eq(Y,V).

% clash

eq(a,b) -> [].

:-option([crw_depth(1),memo_constraints(on)]).
:-sama([]).             % We want saturation by ordered resolution w/o sel.
:-sarp([1-7,10-15]).    % the usual + clausal rewriting  
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.

:-ordering(sto).  % subterm ordering

precedence([f,inp,p1,p2,a,b,tt,eq]).

/*

*/