% theory of joinability
% locality of this theory shows
% that joinability (hence, local confluence)
% can be decided in PTIME
% for ground rewrite systems.

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

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

use(rewrite2).


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


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



:-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



/*

Saturation terminated.

Persisting Clauses:

    1(1) : B==>B
    2(1) : B==>C,C==>D -> B==>D
    3(1) : B==>C,D==>E -> f(B,D)==>f(C,E)
    4(1) : B==>C,D==>E,f(C,E)==>F -> f(B,D)==>F
    5(1) : B==>C,D==>E,F==>f(B,D) -> F==>f(C,E)
    6(1) : join(B,B)
    7(1) : join(B,C) -> join(C,B)
    8(1) : B==>C,join(C,D) -> join(B,D)
    9(1) : join(B,C),join(D,E) -> join(f(B,D),f(C,E))
   11(2) : join(B,C),join(D,E),F==>f(B,D) -> join(F,f(C,E))
   13(2) : B==>C,D==>E,join(f(C,E),F) -> join(f(B,D),F)



Total time: 147210 milliseconds

Number of forward inferences: 21
Number of tableau inferences: 0
Number of kept clauses: 6

*/