use(etas). use(lemmaE3a). use(lemmaE3b). lemmaE3a(S,T,X). % Proof by induction over i: % lim eta^i == eta^* == etas % i=0 etas(u,v) => lemmaE3b(s,s,u,v) , % i -> i+1 ((etas(s,t) and eta(t,w) and etas(u,v) and lemmaE3b(s,t,u,v) and lemmaE3b(t,w,u,v)) => lemmaE3b(s,w,u,v)) -> []. top_predicates_precedence([lemmaE3b,lemmaE3a]). option([var_overlaps(off),search_depth(0)]). :-sarp(+[15]),saci([2]). /* Proof: ====== 2 : eta(A,B) -> eta(app(A,C),app(B,C)) [input] 5 : etas(A,A) [input] 7 : etas(A,B)and eta(B,C) -> etas(A,C) [input] 8 : lemmaE3a(A,B,C)==(etas(A,B)=>etas(abs(A),abs(B))and etas(app(A,C),app(B,C))and etas(app(C,A),app(C,B))) [input] 9 : lemmaE3b(A,B,C,D)==(etas(A,B)=>etas(C,D)=>etas(app(A,C),app(B,D))) [input] 10 : lemmaE3a(A,B,C) [input] 11 : etas(u,v)=>lemmaE3b(s,s,u,v),etas(s,t)and eta(t,w)and etas(u,v)and lemmaE3b(s,t,u,v)and lemmaE3b(t,w,u,v)=>lemmaE3b(s,w,u,v) -> [input] 13 : etas(A,B),eta(B,C) -> etas(A,C) [expansion from 7] 14 : etas(A,B)=>etas(abs(A),abs(B))and etas(app(A,C),app(B,C))and etas(app(C,A),app(C,B)) [reduction of 10 by [8]] 15 : etas(A,B) -> etas(abs(A),abs(B))and etas(app(A,C),app(B,C))and etas(app(C,A),app(C,B)) [expansion from 14] 16 : etas(u,v)=>etas(u,v)=>etas(app(s,u),app(s,v)),etas(s,t)and eta(t,w)and etas(u,v)and(etas(s,t)=>etas(u,v)=>etas(app(s,u),app(t,v)))and(etas(t,w)=>etas(u,v)=>etas(app(t,u),app(w,v)))=>etas(s,w)=>etas(u,v)=>etas(app(s,u),app(w,v)) -> [reduction of 11 by [9,5,L,9,9,9]] 17 : etas(A,B) -> p$199(C,A,B) [expansion from 15] 19 : p$199(A,B,C) -> etas(app(A,B),app(A,C)) [expansion from 15] 20 : p$198,etas(u,v)=>etas(u,v)=>etas(app(s,u),app(s,v)) -> [expansion from 16] 21 : p$198,etas(s,t)and eta(t,w)and etas(u,v)and(etas(s,t)=>etas(u,v)=>etas(app(s,u),app(t,v)))and(etas(t,w)=>etas(u,v)=>etas(app(t,u),app(w,v))) [expansion from 16] 22 : etas(s,w)=>etas(u,v)=>etas(app(s,u),app(w,v)) -> p$198 [expansion from 16] 26 : p$196,p$198 -> [expansion from 20] 27 : p$196,etas(u,v) [expansion from 20] 28 : etas(u,v)=>etas(app(s,u),app(s,v)) -> p$196 [expansion from 20] 29 : etas(app(s,u),app(s,v)) -> p$196 [reduction of 28 by [27,L]] 30 : p$195,p$198 [expansion from 21] 31 : p$195 -> etas(s,t)and eta(t,w)and etas(u,v)and(etas(s,t)=>etas(u,v)=>etas(app(s,u),app(t,v))) [expansion from 21] 34 : p$194 -> p$198 [expansion from 22] 36 : etas(u,v)=>etas(app(s,u),app(w,v)) -> p$194 [expansion from 22] 37 : p$193 -> p$194 [expansion from 36] 38 : p$193,etas(u,v) [expansion from 36] 39 : etas(app(s,u),app(w,v)) -> p$193 [expansion from 36] 42 : p$196,p$199(A,u,v) [negative chaining of 27 from 17] 50 : eta(A,B),etas(C,app(A,D)) -> etas(C,app(B,D)) [negative chaining of 2 from 13] 53 : p$199(s,u,v) -> p$196 [negative chaining of 19 from 29] 54 : p$196 [reduction of 53 by [42]] 55 : p$198 -> [reduction of 26 by [54]] 56 : p$194 -> [reduction of 34 by [55,L]] 57 : p$195 [reduction of 30 by [55,L]] 58 : etas(s,t)and eta(t,w)and etas(u,v)and(etas(s,t)=>etas(u,v)=>etas(app(s,u),app(t,v))) [reduction of 31 by [57]] 60 : p$193 -> [reduction of 37 by [56,L]] 63 : etas(u,v) [reduction of 38 by [60,L]] 65 : etas(app(s,u),app(w,v)) -> [reduction of 39 by [60,L]] 67 : etas(s,t)and eta(t,w)and(etas(s,t)=>etas(app(s,u),app(t,v))) [reduction of 58 by [63,L,63,L]] 69 : etas(s,t)and eta(t,w) [expansion from 67] 70 : etas(s,t)=>etas(app(s,u),app(t,v)) [expansion from 67] 71 : etas(s,t) -> etas(app(s,u),app(t,v)) [expansion from 70] 72 : etas(s,t) [expansion from 69] 73 : eta(t,w) [expansion from 69] 74 : etas(app(s,u),app(t,v)) [reduction of 71 by [72]] 85 : eta(t,A) -> etas(app(s,u),app(A,v)) [negative chaining of 74 from 50] 88 : eta(t,w) -> [negative chaining of 85 from 65] 89 : false [reduction of 88 by [73]] Length = 48, Depth = 18 Total time: 10450 milliseconds Number of forward inferences: 26 Number of tableau inferences: 25 Number of kept clauses: 74 */