% Confluence => UNF

name(unf).

:- dynamic e/2,r/2,s/2.

%domain elements a,b,c
dom(a). dom(b). dom(c).

_ axiom found    :(e(b,c) => goal).
_ axiom assump   :(true => s(a,b),s(a,c)).
_ axiom nf_b(Z)  :(r(b,Z) => false).
_ axiom nf_c(Z)  :(r(c,Z) => false).
_ axiom ref_e(X) :(dom(X) => e(X,X)).
_ axiom sym_e(X,Y) :(e(X,Y) => e(Y,X)).
_ axiom trans_e(X,Y,Z) :(e(X,Y),e(Y,Z) => e(X,Z)).
_ axiom left_congr_of_e(X,Y,Z)  : (e(X,Y),r(Y,Z) => r(X,Z)).
_ axiom e_in_s(X,Y) :(e(X,Y) => s(X,Y)).
_ axiom r_in_s(X,Y) :(r(X,Y) => s(X,Y)).
_ axiom trans_s(X,Y,Z) :(s(X,Y),s(Y,Z) => s(X,Z)).

_ axiom confluence(X,Y,Z) :(s(X,Y),s(X,Z) => dom(U),s(Y,U),s(Z,U)).
% last to avoid infinite path
_ axiom e_or_rs(X,Y) :(s(X,Y) => e(X,Y);dom(Z),r(X,Z),s(Z,Y)). 

%*******************************************************************

enabled(ih(P,Q),[]) :- P=b ; Q=c.
next(ih(P,Q),[],[]).