use(beta). use(lemmaB3a). % Proof by induction over i: % lim beta^i == beta^* == betas % i=0 lemmaB3a(s,s,x), % i -> i+1 ((betas(s,t) and beta(t,w) and lemmaB3a(s,t,x) and lemmaB3a(t,w,x)) => lemmaB3a(s,w,x)) -> []. option([var_overlaps(off),search_depth(0)]). :-sarp(+[15]),saci([2]). /* Proof: ====== 2 : beta(A,B) -> beta(app(C,A),app(C,B)) [input] 3 : beta(A,B) -> beta(app(A,C),app(B,C)) [input] 4 : beta(A,B) -> beta(abs(A),abs(B)) [input] 5 : betas(A,A) [input] 7 : betas(A,B)and beta(B,C) -> betas(A,C) [input] 8 : lemmaB3a(A,B,C)==(betas(A,B)=>betas(abs(A),abs(B))and betas(app(A,C),app(B,C))and betas(app(C,A),app(C,B))) [input] 9 : lemmaB3a(s,s,x),betas(s,t)and beta(t,w)and lemmaB3a(s,t,x)and lemmaB3a(t,w,x)=>lemmaB3a(s,w,x) -> [input] 10 : betas(A,B),beta(B,C) -> betas(A,C) [expansion from 7] 11 : betas(s,t)and beta(t,w)and(betas(s,t)=>betas(abs(s),abs(t))and betas(app(s,x),app(t,x))and betas(app(x,s),app(x,t)))and(betas(t,w)=>betas(abs(t),abs(w))and betas(app(t,x),app(w,x))and betas(app(x,t),app(x,w)))=>betas(s,w)=>betas(abs(s),abs(w))and betas(app(s,x),app(w,x))and betas(app(x,s),app(x,w)) -> [reduction of 9 by [8,5,5,5,L,L,5,L,8,8,8]] 12 : betas(s,t)and beta(t,w)and(betas(s,t)=>betas(abs(s),abs(t))and betas(app(s,x),app(t,x))and betas(app(x,s),app(x,t)))and(betas(t,w)=>betas(abs(t),abs(w))and betas(app(t,x),app(w,x))and betas(app(x,t),app(x,w))) [expansion from 11] 13 : betas(s,w)=>betas(abs(s),abs(w))and betas(app(s,x),app(w,x))and betas(app(x,s),app(x,w)) -> [expansion from 11] 14 : betas(s,t)and beta(t,w)and(betas(s,t)=>betas(abs(s),abs(t))and betas(app(s,x),app(t,x))and betas(app(x,s),app(x,t))) [expansion from 12] 18 : betas(abs(s),abs(w))and betas(app(s,x),app(w,x))and betas(app(x,s),app(x,w)) -> [expansion from 13] 19 : betas(app(x,s),app(x,w)),betas(abs(s),abs(w)),betas(app(s,x),app(w,x)) -> [expansion from 18] 20 : betas(s,t)and beta(t,w) [expansion from 14] 21 : betas(s,t)=>betas(abs(s),abs(t))and betas(app(s,x),app(t,x))and betas(app(x,s),app(x,t)) [expansion from 14] 22 : betas(s,t) -> betas(abs(s),abs(t))and betas(app(s,x),app(t,x))and betas(app(x,s),app(x,t)) [expansion from 21] 26 : betas(s,t) [expansion from 20] 27 : beta(t,w) [expansion from 20] 28 : betas(abs(s),abs(t))and betas(app(s,x),app(t,x))and betas(app(x,s),app(x,t)) [reduction of 22 by [26]] 29 : betas(abs(s),abs(t))and betas(app(s,x),app(t,x)) [expansion from 28] 30 : betas(app(x,s),app(x,t)) [expansion from 28] 31 : betas(abs(s),abs(t)) [expansion from 29] 32 : betas(app(s,x),app(t,x)) [expansion from 29] 36 : beta(A,B),betas(C,abs(A)) -> betas(C,abs(B)) [negative chaining of 4 from 10] 38 : beta(A,B),betas(C,app(D,A)) -> betas(C,app(D,B)) [negative chaining of 2 from 10] 39 : beta(A,B),betas(C,app(A,D)) -> betas(C,app(B,D)) [negative chaining of 3 from 10] 40 : beta(t,A) -> betas(abs(s),abs(A)) [negative chaining of 31 from 36] 41 : beta(t,A) -> betas(app(x,s),app(x,A)) [negative chaining of 30 from 38] 44 : beta(t,A) -> betas(app(s,x),app(A,x)) [negative chaining of 32 from 39] 46 : beta(t,w),betas(app(s,x),app(w,x)),betas(app(x,s),app(x,w)) -> [negative chaining of 40 from 19] 48 : false [reduction of 46 by [27,44,27,41,27]] Length = 32, Depth = 12 Total time: 4140 milliseconds Number of forward inferences: 13 Number of tableau inferences: 17 Number of kept clauses: 40 */