% original version at http://www.ii.uib.no/~bezem/GL/nl.in
% induction step in Newman's Lemma

:- 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,X] := s(b,X),s(c,X) => answer((s(b,X),s(c,X))).
[] := answer(_) => goal.

[assump] := true => s(a,b),s(a,c).
[ref_e,X] := dom(X) => e(X,X).
[sym_e,X,Y] := e(X,Y) => e(Y,X).
[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).

[lo_cfl,X,Y,Z] := r(X,Y),r(X,Z) => dom(U),s(Y,U),s(Z,U).
[ih_cfl,X,Y,Z] := r(a,X),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).