% induction step in Newman's Lemma

%note('domain elements').
true => exists(a), exists(b), exists(c).  %1

%note('goal found').
s(b,X),s(c,X) => goal.  %2

%note('assumption').
true => s(a,b),s(a,c).  %3

%note('e reflexive').
exists(X) => e(X,X).  %4

%note('e symmetric').
e(X,Y) => e(Y,X).  %5

%note('e(,) => s(,)').
e(X,Y) => s(X,Y).  %6

%note('r(,) => s(,)').
r(X,Y) => s(X,Y).  %7

%note('s transitive').
s(X,Y),s(Y,Z) => s(X,Z).  %8

%note('lo_cfl').
r(X,Y),r(X,Z) => exists(U),s(Y,U),s(Z,U).  %9

%note('ih_cfl').
r(a,X),s(X,Y),s(X,Z) => exists(U),s(Y,U),s(Z,U).  %10

%note('s => e ; ... r,s').
s(X,Y) => e(X,Y) ; exists(Z),r(X,Z),s(Z,Y).  %11