% original version at http://www.csupomona.edu/~jrfisher/www/geolog/unf.in
% Confluence => UNF

:- op(1200,xfx,':=').
:- op(1199,xfx,'=>').

:- dynamic(e/2).
:- dynamic(r/2).
:- dynamic(s/2).
:- dynamic(dom/1).
:- dynamic(answer/1).

flag(keywords).
flag(quiet).
flag(quick).

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

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

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