% binary variant of ground rewriting
% locality of this theory shows
% that reachability can be decided in PTIME
% for ground rewrite systems.

:-op(200,xfx,==>).

predicates([==>,join,eq]).
precedence([f,==>,join,eq]).

:-option([special_relations(off)]).





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),f(Y,V)).          % a
eq(X,Y), eq(U,V), eq(f(X,U),Z) -> eq(f(Y,V),Z).   % b
eq(X,Y), eq(U,V), X==>U -> Y==>V.





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



:-option([crw_depth(1),memo_constraints(on)]).
:-sarp([1-7,10-15]). % the usual + clausal rewriting  
:-sama([]).
%:-saci([2]).        % not needed and wouldn't terminate anymore
:-sams([3,19]).      % messages about redundancy proofs by clausal rewrtng.
:-ordering(sto).     % subterm ordering


/*

*/