% induction step in Newman's Lemma name(nl). :- dynamic e/2,r/2,s/2. %domain elements a,b,c dom(a). dom(b). dom(c). _ axiom found(X) :(s(b,X),s(c,X) => goal). _ axiom assump :(true => s(a,b),s(a,c)). _ axiom ref_e(X) :(dom(X) => e(X,X)). _ axiom sym_e(X,Y) :(e(X,Y) => e(Y,X)). _ 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 lo_cfl(X,Y,Z) :(r(X,Y),r(X,Z) => dom(U),s(Y,U),s(Z,U)). _ axiom 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 _ axiom e_or_rs(X,Y) :(s(X,Y) => e(X,Y);dom(Z),r(X,Z),s(Z,Y)).