use(beta). use(pbeta). use(lemmaB3a). use(lemmaB3b). % Proof by induction over pbeta: % pbeta ist Teilmenge von betas lemmaB3a(S,T,X). lemmaB3b(S,T,U,V). goal %Induktionsanfang pbeta(var(i),var(i)) => betas(var(i),var(i)), %Induktionsschritt ((pbeta(s,t) and betas(s,t)) => betas(abs(s),abs(t))), %Die letzten beiden Induktionsschritte zusammengefasst ((pbeta(s,t) and betas(s,t) and pbeta(u,v) and betas(u,v)) => betas(app(abs(s),u),subst(t,0,v)) and betas(app(s,u),app(t,v))) -> []. top_predicates_precedence([lemmaB3a,lemmaB3b,pbeta,beta,betas]). option([var_overlaps(off),search_depth(1)]). :-sarp(+[15]),saci([2]). /* Proof: ====== 1 : beta(app(abs(A),B),subst(A,0,B)) [input] 5 : betas(A,A) [input] 7 : betas(A,B)and beta(B,C) -> betas(A,C) [input] 12 : pbeta(A,A) [input] 13 : 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] 14 : lemmaB3b(A,B,C,D)==(betas(A,B)=>betas(C,D)=>betas(app(A,C),app(B,D))) [input] 15 : lemmaB3a(A,B,C) [input] 16 : lemmaB3b(A,B,C,D) [input] 17 + pbeta(var(i),var(i))=>betas(var(i),var(i)),pbeta(s,t)and betas(s,t)=>betas(abs(s),abs(t)),pbeta(s,t)and betas(s,t)and pbeta(u,v)and betas(u,v)=>betas(app(abs(s),u),subst(t,0,v))and betas(app(s,u),app(t,v)) -> [input] 18 : betas(A,B),beta(B,C) -> betas(A,C) [expansion from 7] 21 : betas(A,B)=>betas(abs(A),abs(B))and betas(app(A,C),app(B,C))and betas(app(C,A),app(C,B)) [reduction of 15 by [13]] 22 : betas(A,B) -> betas(abs(A),abs(B))and betas(app(A,C),app(B,C))and betas(app(C,A),app(C,B)) [expansion from 21] 23 : betas(A,B)=>betas(C,D)=>betas(app(A,C),app(B,D)) [reduction of 16 by [14]] 24 : betas(A,B),betas(C,D) -> betas(app(A,C),app(B,D)) [expansion from 23] 25 + pbeta(s,t)and betas(s,t)and pbeta(u,v)and betas(u,v)=>betas(app(abs(s),u),subst(t,0,v))and betas(app(s,u),app(t,v)),pbeta(s,t)and betas(s,t)=>betas(abs(s),abs(t)) -> [reduction of 17 by [5,12,L]] 26 : betas(A,B) -> p$499(C,A,B) [expansion from 22] 27 : p$499(A,B,C) -> betas(abs(B),abs(C))and betas(app(B,A),app(C,A)) [expansion from 22] 29 + p$498,pbeta(s,t)and betas(s,t)=>betas(abs(s),abs(t)) -> [expansion from 25] 30 + p$498,pbeta(s,t)and betas(s,t)and pbeta(u,v)and betas(u,v) [expansion from 25] 31 + betas(app(abs(s),u),subst(t,0,v))and betas(app(s,u),app(t,v)) -> p$498 [expansion from 25] 32 + betas(app(abs(s),u),subst(t,0,v)),betas(app(s,u),app(t,v)) -> p$498 [expansion from 31] 33 : p$499(A,B,C) -> p$497(A,B,C) [expansion from 27] 34 : p$497(A,B,C) -> betas(abs(B),abs(C)) [expansion from 27] 36 + p$496,p$498 -> [expansion from 29] 37 + p$496,pbeta(s,t)and betas(s,t) [expansion from 29] 38 + betas(abs(s),abs(t)) -> p$496 [expansion from 29] 39 + p$495,p$498 [expansion from 30] 40 + p$495 -> pbeta(s,t)and betas(s,t)and pbeta(u,v) [expansion from 30] 41 + p$495 -> betas(u,v) [expansion from 30] 42 + p$494,p$496 [expansion from 37] 44 + p$494 -> betas(s,t) [expansion from 37] 45 + p$498,betas(u,v) [negative chaining of 39 from 41] 47 + p$496,betas(s,t) [negative chaining of 42 from 44] 50 + p$498,pbeta(s,t)and betas(s,t)and pbeta(u,v) [negative chaining of 39 from 40] 51 + p$493,p$498 [expansion from 50] 52 + p$493 -> pbeta(s,t)and betas(s,t) [expansion from 50] 55 + p$498,pbeta(s,t)and betas(s,t) [negative chaining of 51 from 52] 56 + p$494,p$498 [expansion from 55] 58 + p$498,betas(s,t) [negative chaining of 56 from 44] 63 + p$496,p$499(A,s,t) [negative chaining of 47 from 26] 64 + p$498,p$499(A,s,t) [negative chaining of 58 from 26] 65 + p$497(A,s,t) -> p$496 [negative chaining of 34 from 38] 67 + p$496 [reduction of 65 by [33,63]] 68 + p$498 -> [reduction of 36 by [67]] 70 + betas(u,v) [reduction of 45 by [68,L]] 75 + betas(s,t) [reduction of 58 by [68,L]] 77 + p$499(A,s,t) [reduction of 64 by [68,L]] 78 + betas(app(abs(s),u),subst(t,0,v)) -> [reduction of 32 by [24,70,75,68,L]] 81 : betas(A,app(abs(B),C)) -> betas(A,subst(B,0,C)) [negative chaining of 1 from 18] 87 + betas(app(abs(s),u),app(abs(t),v)) -> [negative chaining of 81 from 78] 89 + betas(abs(s),abs(t)),betas(u,v) -> [negative chaining of 24 from 87] 90 + betas(abs(s),abs(t)) -> [reduction of 89 by [70]] 91 + p$497(A,s,t) -> [negative chaining of 34 from 90] 92 + false [reduction of 91 by [33,77]] Length = 54, Depth = 16 Total time: 2980 milliseconds Number of forward inferences: 30 Number of tableau inferences: 22 Number of kept clauses: 76 */