use(subst). use(beta). use(etas). use(subst_lemmas). use(comm_lemma). use(lemmaE2). use(lemmaE7). use(lemmaB1). use(lemmaB2). %benoetigte Lemmas lemmaE7(S,T,U,I). lemmaF1(S,T,U,I). lemmaE2(S,T,U,I). lemmaB1(S,T,I). lemmaB2(S,T,U,I). etas(S,T) -> etas(app(S,U),app(T,U)). etas(S,T) -> etas(app(V,S),app(V,T)). etas(S,T) -> etas(abs(S),abs(T)). %Definition von betar betar(S,T) == (beta(S,T) or S=T). %Beweis per Induktion ueber beta goal % ***Induktionsanfang***: beta(app(abs(S),T),subst(S,0,T)) % Fall S=app(s,var(0)) und % eta(app(abs(app(s,var(0)))),app(subst(s,0,u),t)) (~free(s,0) => comm_lemma(app(abs(app(s,var(0))),t), subst(app(s,var(0)),0,t),app(subst(s,0,u),t))), % Fall S=s und eta(s,t) -> eta(app(abs(s),u),app(abs(t),u)) (eta(s,t) => comm_lemma(app(abs(s),u),subst(s,0,u),app(abs(t),u))), % Fall S=s und eta(t,x) -> eta(app(abs(s),t),app(abs(s),x)) (eta(t,x) => comm_lemma(app(abs(s),t),subst(s,0,t),app(abs(s),x))), % ***Induktionsschritt***: beta(S,T) -> beta(abs(S),abs(T)) % Fall eta(s,x) -> eta(abs(s),abs(x)) ((comm_lemma(s,t,x) and beta(s,t) and eta(s,x)) => comm_lemma(abs(s),abs(t),abs(x))), % Fall S=app(s,var(0)) und ~free(s,0) -> eta(abs(app(s,var(0))),subst(s,0,u)) ((~free(s,0) and beta(s,t)) => comm_lemma(abs(app(s,var(0))),abs(app(t,var(0))),subst(s,0,u))), % Weiterer Fall siehe Datei "commb" % ***Induktionsschritt***: beta(S,T) -> beta(app(S,U),app(T,U)) and % beta (app(U,S),app(U,T)) % zwei Faelle fuer eta(s,x) -> % eta(app(s,u),app(x,u)) and eta(app(u,s),app(u,x)) % und zwei fuer eta(u,v) -> % eta(app(s,u),app(s,v)) and eta(app(u,s),app(v,s)) ((comm_lemma(s,t,x) and beta(s,t) and eta(s,x) and eta(u,v)) => (comm_lemma(app(s,u),app(t,u),app(x,u)) and comm_lemma(app(u,s),app(u,t),app(u,x)) and comm_lemma(app(s,u),app(t,u),app(s,v)) and comm_lemma(app(u,s),app(u,t),app(v,s)) )) -> []. top_predicates_precedence([comm_lemma,betar,lemmaF1,etas]). option([var_overlaps(off),search_depth(3),iterative_saturation(on)]). :-sarp(+[15]),saci([2]). /* Proof: ====== 15 : subst(var(A),A,B)=B [input] 17 : subst(app(A,B),C,D)=app(subst(A,C,D),subst(B,C,D)) [input] 26 : beta(app(abs(A),B),subst(A,0,B)) [input] 27 : beta(A,B) -> beta(app(C,A),app(C,B)) [input] 28 : beta(A,B) -> beta(app(A,C),app(B,C)) [input] 29 : beta(A,B) -> beta(abs(A),abs(B)) [input] 33 : ~free(A,0) -> eta(abs(app(A,var(0))),subst(A,0,B)) [input] 34 : eta(A,B) -> eta(app(A,C),app(B,C)) [input] 35 : eta(A,B) -> eta(app(C,A),app(C,B)) [input] 36 : eta(A,B) -> eta(abs(A),abs(B)) [input] 37 : etas(A,A) [input] 38 : eta(A,B) -> etas(A,B) [input] 39 : etas(A,B)and eta(B,C) -> etas(A,C) [input] 46 : lemmaF1(A,B,C,D)==(~free(A,D)and 0=subst(A,D,B)=subst(A,D,C)) [input] 47 : comm_lemma(A,B,C)==(beta(A,B)and eta(A,C)=>?D.(etas(B,D)and betar(C,D))) [input] 48 : lemmaE2(A,B,C,D)==(0=eta(subst(A,D,C),subst(B,D,C))) [input] 49 : lemmaE7(A,B,C,D)==(0=etas(subst(C,D,A),subst(C,D,B))) [input] 50 : lemmaB1(A,B,C)==(0=beta(A,B)=>free(B,C)=>free(A,C)) [input] 51 : lemmaB2(A,B,C,D)==(0=beta(A,B)=>beta(subst(A,D,C),subst(B,D,C))) [input] 52 : lemmaE7(A,B,C,D) [input] 53 : lemmaF1(A,B,C,D) [input] 54 : lemmaE2(A,B,C,D) [input] 55 : lemmaB1(A,B,C) [input] 56 : lemmaB2(A,B,C,D) [input] 57 : etas(A,B) -> etas(app(A,C),app(B,C)) [input] 58 : etas(A,B) -> etas(app(C,A),app(C,B)) [input] 59 : etas(A,B) -> etas(abs(A),abs(B)) [input] 60 : betar(A,B)==(beta(A,B)or A=B) [input] 61 + ~free(s,0)=>comm_lemma(app(abs(app(s,var(0))),t),subst(app(s,var(0)),0,t),app(subst(s,0,u),t)),eta(s,t)=>comm_lemma(app(abs(s),u),subst(s,0,u),app(abs(t),u)),eta(t,x)=>comm_lemma(app(abs(s),t),subst(s,0,t),app(abs(s),x)),comm_lemma(s,t,x)and beta(s,t)and eta(s,x)=>comm_lemma(abs(s),abs(t),abs(x)),~free(s,0)and beta(s,t)=>comm_lemma(abs(app(s,var(0))),abs(app(t,var(0))),subst(s,0,u)),comm_lemma(s,t,x)and beta(s,t)and eta(s,x)and eta(u,v)=>comm_lemma(app(s,u),app(t,u),app(x,u))and comm_lemma(app(u,s),app(u,t),app(u,x))and comm_lemma(app(s,u),app(t,u),app(s,v))and comm_lemma(app(u,s),app(u,t),app(v,s)) -> [input] 69 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0) [expansion from 33] 70 : etas(A,B),eta(B,C) -> etas(A,C) [expansion from 39] 71 : ~free(A,B)and 0=subst(A,B,C)=subst(A,B,D) [reduction of 53 by [46]] 72 : 0= subst(B,A,C)=subst(B,A,D),free(B,A) [expansion from 71] 73 : A<0,subst(B,A,C)=subst(B,A,D),free(B,A) [totality resolution from 72] 74 : subst(A,B,C)=f$0(A,B),B<0,free(A,B) [variable elimination from 73] 75 : subst(A,B,C)=f$0(A,B),B<0,free(A,B) [variable elimination from 73] 76 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 54 by [48]] 77 : 0= eta(subst(B,A,D),subst(C,A,D)) [expansion from 76] 78 : eta(A,B) -> C<0,eta(subst(A,C,D),subst(B,C,D)) [totality resolution from 77] 79 : 0=beta(B,C)=>free(C,A)=>free(B,A) [reduction of 55 by [50]] 80 : 0= free(B,A) [expansion from 79] 81 : beta(A,B),free(B,C) -> C<0,free(A,C) [totality resolution from 80] 82 : 0=beta(B,C)=>beta(subst(B,A,D),subst(C,A,D)) [reduction of 56 by [51]] 83 : 0= beta(subst(B,A,D),subst(C,A,D)) [expansion from 82] 84 : beta(A,B) -> C<0,beta(subst(A,C,D),subst(B,C,D)) [totality resolution from 83] 85 + ~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)),(beta(s,t)and eta(s,x)=>?B.(etas(t,B)and(beta(x,B)or x=B)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?C.(etas(abs(t),C)and(beta(abs(x),C)or abs(x)=C)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?D.(etas(subst(s,0,t),D)and(beta(app(abs(s),x),D)or app(abs(s),x)=D)),eta(s,t)=>eta(app(abs(s),u),app(abs(t),u))=>?E.(etas(subst(s,0,u),E)and(beta(app(abs(t),u),E)or app(abs(t),u)=E)),~free(s,0)=>beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?F.(etas(app(subst(s,0,t),t),F)and(beta(app(subst(s,0,u),t),F)or app(subst(s,0,u),t)=F)),(beta(s,t)and eta(s,x)=>?G.(etas(t,G)and(beta(x,G)or x=G)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?H.(etas(app(t,u),H)and(beta(app(x,u),H)or app(x,u)=H)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?I.(etas(app(u,t),I)and(beta(app(u,x),I)or app(u,x)=I)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?J.(etas(app(t,u),J)and(beta(app(s,v),J)or app(s,v)=J)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?K.(etas(app(u,t),K)and(beta(app(v,s),K)or app(v,s)=K))) -> [reduction of 61 by [17,15,47,60,47,60,26,L,47,60,26,L,47,60,47,60,47,60,47,60,47,60,47,60,47,60,47,60]] 87 : 0=etas(subst(D,A,B),subst(D,A,C)) [reduction of 49 by [52]] 88 : 0= etas(subst(D,A,B),subst(D,A,C)) [expansion from 87] 89 : eta(A,B) -> C<0,etas(subst(D,C,A),subst(D,C,B)) [totality resolution from 88] 90 + p$199,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?B.(etas(abs(t),B)and(beta(abs(x),B)or abs(x)=B)),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?C.(etas(abs(app(t,var(0))),C)and(beta(subst(s,0,u),C)or subst(s,0,u)=C)),(beta(s,t)and eta(s,x)=>?D.(etas(t,D)and(beta(x,D)or x=D)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?E.(etas(app(t,u),E)and(beta(app(x,u),E)or app(x,u)=E)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?F.(etas(app(u,t),F)and(beta(app(u,x),F)or app(u,x)=F)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?G.(etas(app(t,u),G)and(beta(app(s,v),G)or app(s,v)=G)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?H.(etas(app(u,t),H)and(beta(app(v,s),H)or app(v,s)=H))),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?I.(etas(subst(s,0,t),I)and(beta(app(abs(s),x),I)or app(abs(s),x)=I)),~free(s,0)=>beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?J.(etas(app(subst(s,0,t),t),J)and(beta(app(subst(s,0,u),t),J)or app(subst(s,0,u),t)=J)) -> [expansion from 85] 91 + p$199,eta(s,t) [expansion from 85] 92 + eta(app(abs(s),u),app(abs(t),u))=>?A.(etas(subst(s,0,u),A)and(beta(app(abs(t),u),A)or app(abs(t),u)=A)) -> p$199 [expansion from 85] 93 + ?A.(etas(subst(s,0,u),A)and(beta(app(abs(t),u),A)or app(abs(t),u)=A)) -> p$199 [reduction of 92 by [34,36,91,L]] 94 + etas(subst(s,0,u),A),beta(app(abs(t),u),A)or app(abs(t),u)=A -> p$199 [expansion from 93] 95 + p$198,~free(s,0)=>beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?A.(etas(app(subst(s,0,t),t),A)and(beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A)),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?B.(etas(abs(app(t,var(0))),B)and(beta(subst(s,0,u),B)or subst(s,0,u)=B)),(beta(s,t)and eta(s,x)=>?C.(etas(t,C)and(beta(x,C)or x=C)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?D.(etas(abs(t),D)and(beta(abs(x),D)or abs(x)=D)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?E.(etas(subst(s,0,t),E)and(beta(app(abs(s),x),E)or app(abs(s),x)=E)),p$199 -> [expansion from 90] 96 + p$198,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)and eta(u,v) [expansion from 90] 97 + (beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?A.(etas(app(t,u),A)and(beta(app(x,u),A)or app(x,u)=A)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?B.(etas(app(u,t),B)and(beta(app(u,x),B)or app(u,x)=B)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?C.(etas(app(t,u),C)and(beta(app(s,v),C)or app(s,v)=C)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?D.(etas(app(u,t),D)and(beta(app(v,s),D)or app(v,s)=D))) -> p$198 [expansion from 90] 98 + beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?A.(etas(app(u,t),A)and(beta(app(v,s),A)or app(v,s)=A)),beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?B.(etas(app(t,u),B)and(beta(app(s,v),B)or app(s,v)=B)),beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?C.(etas(app(t,u),C)and(beta(app(x,u),C)or app(x,u)=C)),beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?D.(etas(app(u,t),D)and(beta(app(u,x),D)or app(u,x)=D)) -> p$198 [expansion from 97] 99 + p$197,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?B.(etas(abs(t),B)and(beta(abs(x),B)or abs(x)=B)),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?C.(etas(abs(app(t,var(0))),C)and(beta(subst(s,0,u),C)or subst(s,0,u)=C)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?D.(etas(subst(s,0,t),D)and(beta(app(abs(s),x),D)or app(abs(s),x)=D)),p$198,p$199 -> [expansion from 95] 100 + p$197,~free(s,0) [expansion from 95] 101 + beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?A.(etas(app(subst(s,0,t),t),A)and(beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A)) -> p$197 [expansion from 95] 102 + free(s,0) -> p$197 [expansion from 100] 103 + beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))=>?A.(etas(app(subst(s,0,t),t),A)and(beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A)) -> p$197 [reduction of 101 by [34,69,102,L,L]] 104 + p$196,p$198 [expansion from 96] 105 + p$196 -> (beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x) [expansion from 96] 106 + p$196 -> eta(u,v) [expansion from 96] 107 + p$195,beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)),beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)),beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.(etas(app(u,t),C)and(beta(app(u,x),C)or app(u,x)=C)) -> p$198 [expansion from 98] 109 + ?A.(etas(app(u,t),A)and(beta(app(v,s),A)or app(v,s)=A)) -> p$195 [expansion from 98] 110 + etas(app(u,t),A),beta(app(v,s),A)or app(v,s)=A -> p$195 [expansion from 109] 111 + p$194 -> p$197 [expansion from 103] 113 + ?A.(etas(app(subst(s,0,t),t),A)and(beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A)) -> p$194 [expansion from 103] 114 + etas(app(subst(s,0,t),t),A),beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A -> p$194 [expansion from 113] 115 + p$193,beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)),beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?B.(etas(app(u,t),B)and(beta(app(u,x),B)or app(u,x)=B)),p$195 -> p$198 [expansion from 107] 117 + ?A.(etas(app(t,u),A)and(beta(app(x,u),A)or app(x,u)=A)) -> p$193 [expansion from 107] 118 + etas(app(t,u),A),beta(app(x,u),A)or app(x,u)=A -> p$193 [expansion from 117] 125 + p$198,eta(u,v) [negative chaining of 104 from 106] 144 + eta(app(u,t),A),beta(app(v,s),A)or app(v,s)=A -> p$195 [negative chaining of 38 from 110] 152 + etas(t,A),beta(app(x,u),app(A,u))or app(x,u)=app(A,u) -> p$193 [negative chaining of 57 from 118] 158 + eta(u,A),beta(app(v,s),app(A,t))or app(v,s)=app(A,t) -> p$195 [negative chaining of 34 from 144] 170 + beta(app(v,s),app(v,t))or app(v,s)=app(v,t) -> p$198,p$195 [negative chaining of 125 from 158] 171 + p$188 -> p$198,p$195 [expansion from 170] 172 + beta(app(v,s),app(v,t)) -> p$188 [expansion from 170] 174 + beta(s,t) -> p$188 [negative chaining of 27 from 172] 180 + eta(subst(s,0,u),A),beta(app(abs(t),u),A)or app(abs(t),u)=A -> p$199 [negative chaining of 38 from 94] 198 : eta(A,B),eta(B,C) -> etas(A,C) [negative chaining of 38 from 70] 203 + eta(app(t,u),A),eta(A,B),beta(app(x,u),B)or app(x,u)=B -> p$193 [negative chaining of 198 from 118] 214 + beta(app(x,u),A) -> p$184(A) [expansion from 203] 229 + beta(x,A) -> p$184(app(A,u)) [negative chaining of 28 from 214] 248 + beta(app(subst(s,0,u),t),app(subst(s,0,t),t))or app(subst(s,0,u),t)=app(subst(s,0,t),t) -> p$194 [negative chaining of 37 from 114] 253 + p$182 -> p$194 [expansion from 248] 255 + app(subst(s,0,u),t)=app(subst(s,0,t),t) -> p$182 [expansion from 248] 456 + subst(s,0,A)=f$0(s,0),p$197 {[conj([free(s,0)>A],[],[])]} [negative chaining of 74 from 102] 468 : beta(A,B) -> subst(B,C,D)=f$0(B,C),C<0,free(A,C),C<0 {[conj([free(B,C)>D],[],[])]} [negative chaining of 74 from 81] 486 : beta(A,B) -> subst(B,C,D)=f$0(B,C),free(A,C),C<0 {[conj([free(B,C)>D],[],[])]} [condensement of 468] 502 + app(f$0(s,0),t)=app(subst(s,0,t),t) -> p$197,p$182 [negative chaining of 456 from 255] 520 + p$197 [reduction of 502 by [456,L,253,111,L,L]] 521 + ~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)),(beta(s,t)and eta(s,x)=>?B.(etas(t,B)and(beta(x,B)or x=B)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?C.(etas(abs(t),C)and(beta(abs(x),C)or abs(x)=C)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?D.(etas(subst(s,0,t),D)and(beta(app(abs(s),x),D)or app(abs(s),x)=D)),p$198,p$199 -> [reduction of 99 by [520]] 752 + eta(s,A),beta(app(abs(t),u),subst(A,0,u))or app(abs(t),u)=subst(A,0,u) -> p$199 [negative chaining of 78 from 180] 776 + beta(app(abs(t),u),subst(t,0,u))or app(abs(t),u)=subst(t,0,u) -> p$199,p$199 [negative chaining of 91 from 752] 777 + beta(app(abs(t),u),subst(t,0,u))or app(abs(t),u)=subst(t,0,u) -> p$199 [condensement of 776] 778 + p$199 [reduction of 777 by [26,L]] 779 + ~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)),(beta(s,t)and eta(s,x)=>?B.(etas(t,B)and(beta(x,B)or x=B)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?C.(etas(abs(t),C)and(beta(abs(x),C)or abs(x)=C)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?D.(etas(subst(s,0,t),D)and(beta(app(abs(s),x),D)or app(abs(s),x)=D)),p$198 -> [reduction of 521 by [778]] 871 + p$198,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x) [negative chaining of 104 from 105] 872 + p$175,p$198 [expansion from 871] 873 + p$175 -> (beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t) [expansion from 871] 874 + p$175 -> eta(s,x) [expansion from 871] 875 + p$198,eta(s,x) [negative chaining of 872 from 874] 881 + p$198,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t) [negative chaining of 872 from 873] 882 + p$198,(beta(s,t)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t) [reduction of 881 by [875,L]] 883 + p$174,p$198 [expansion from 882] 884 + p$174 -> beta(s,t)=>?A.(etas(t,A)and(beta(x,A)or x=A)) [expansion from 882] 885 + p$174 -> beta(s,t) [expansion from 882] 886 + p$174,beta(s,t) -> ?A.(etas(t,A)and(beta(x,A)or x=A)) [expansion from 884] 887 + p$198,beta(s,t) [negative chaining of 883 from 885] 888 + p$198,p$188 [negative chaining of 887 from 174] 894 + p$198,p$198,p$195 [negative chaining of 888 from 171] 895 + p$198,p$195 [condensement of 894] 898 + p$174 -> p$198,?A.(etas(t,A)and(beta(x,A)or x=A)) [negative chaining of 887 from 886] 899 + ?A.(etas(t,A)and(beta(x,A)or x=A)),p$198 [reduction of 898 by [883]] 900 + p$173,p$198 [expansion from 899] 901 + p$173 -> etas(t,s$3)and(beta(x,s$3)or x=s$3) [expansion from 899] 902 + p$198,etas(t,s$3)and(beta(x,s$3)or x=s$3) [negative chaining of 900 from 901] 903 + p$172,p$198 [expansion from 902] 904 + p$172 -> etas(t,s$3) [expansion from 902] 905 + p$172 -> beta(x,s$3)or x=s$3 [expansion from 902] 906 + p$172 -> beta(x,s$3),x=s$3 [expansion from 905] 907 + p$198,etas(t,s$3) [negative chaining of 903 from 904] 909 + beta(app(x,u),app(s$3,u))or app(x,u)=app(s$3,u) -> p$198,p$193 [negative chaining of 907 from 152] 915 + p$184(app(s$3,u)) -> p$198,p$193 [expansion from 909] 917 + p$198,beta(x,s$3),s$3=x [negative chaining of 903 from 906] 919 + p$198,s$3=x,p$184(app(s$3,u)) [negative chaining of 917 from 229] 926 + p$198,s$3=x,p$198,p$193 [negative chaining of 919 from 915] 927 + s$3=x,p$198,p$193 [condensement of 926] 928 + etas(t,x),p$198,p$193,p$198 [chaining of 927 from 907] 933 + etas(t,x),p$193,p$198 [condensement of 928] 934 + p$198,p$193 [reduction of 933 by [152,L,L,L]] 939 + p$171,beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?A.(etas(app(u,t),A)and(beta(app(u,x),A)or app(u,x)=A)),p$193,p$195 -> p$198 [expansion from 115] 941 + ?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)) -> p$171 [expansion from 115] 942 + ?A.(etas(app(u,t),A)and(beta(app(u,x),A)or app(u,x)=A)),p$171 -> p$198 [reduction of 939 by [35,875,27,887,L,L,934,895]] 943 + p$171,etas(app(u,t),A),beta(app(u,x),A)or app(u,x)=A -> p$198 [expansion from 942] 944 + etas(app(t,u),A),beta(app(s,v),A)or app(s,v)=A -> p$171 [expansion from 941] 945 + p$170(A),etas(app(u,t),A),p$171 -> p$198 [expansion from 943] 946 + beta(app(u,x),A) -> p$170(A) [expansion from 943] 947 + app(u,x)=A -> p$170(A) [expansion from 943] 951 + p$170(app(u,x)) [reflexivity resolution from 947] 954 + beta(x,A) -> p$170(app(u,A)) [negative chaining of 27 from 946] 956 + p$198,s$3=x,p$170(app(u,s$3)) [negative chaining of 917 from 954] 970 + eta(app(t,u),A),beta(app(s,v),A)or app(s,v)=A -> p$171 [negative chaining of 38 from 944] 995 + eta(u,A),beta(app(s,v),app(t,A))or app(s,v)=app(t,A) -> p$171 [negative chaining of 35 from 970] 1024 + beta(app(s,v),app(t,v))or app(s,v)=app(t,v) -> p$198,p$171 [negative chaining of 125 from 995] 1025 + p$171,p$198 [reduction of 1024 by [28,887,L]] 1029 + etas(t,A),p$170(app(u,A)),p$171 -> p$198 [negative chaining of 58 from 945] 1037 + etas(t,A),p$170(app(u,A)) -> p$198 [reduction of 1029 by [1025]] 1052 + p$170(app(u,s$3)) -> p$198,p$198 [negative chaining of 907 from 1037] 1053 + p$170(app(u,s$3)) -> p$198 [condensement of 1052] 1055 + p$198,s$3=x,p$198 [negative chaining of 956 from 1053] 1057 + s$3=x,p$198 [condensement of 1055] 1058 + etas(t,x),p$198,p$198 [chaining of 1057 from 907] 1067 + etas(t,x),p$198 [condensement of 1058] 1068 + p$198 [reduction of 1067 by [1037,951,L]] 1077 + ~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)),(beta(s,t)and eta(s,x)=>?B.(etas(t,B)and(beta(x,B)or x=B)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?C.(etas(abs(t),C)and(beta(abs(x),C)or abs(x)=C)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?D.(etas(subst(s,0,t),D)and(beta(app(abs(s),x),D)or app(abs(s),x)=D)) -> [reduction of 779 by [1068]] 1078 + p$166,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?B.(etas(abs(t),B)and(beta(abs(x),B)or abs(x)=B)),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?C.(etas(abs(app(t,var(0))),C)and(beta(subst(s,0,u),C)or subst(s,0,u)=C)) -> [expansion from 1077] 1079 + p$166,eta(t,x) [expansion from 1077] 1080 + eta(app(abs(s),t),app(abs(s),x))=>?A.(etas(subst(s,0,t),A)and(beta(app(abs(s),x),A)or app(abs(s),x)=A)) -> p$166 [expansion from 1077] 1081 + ?A.(etas(subst(s,0,t),A)and(beta(app(abs(s),x),A)or app(abs(s),x)=A)) -> p$166 [reduction of 1080 by [35,1079,L]] 1082 + etas(subst(s,0,t),A),beta(app(abs(s),x),A)or app(abs(s),x)=A -> p$166 [expansion from 1081] 1083 + p$165,~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)),p$166 -> [expansion from 1078] 1084 + p$165,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x) [expansion from 1078] 1085 + beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?A.(etas(abs(t),A)and(beta(abs(x),A)or abs(x)=A)) -> p$165 [expansion from 1078] 1086 + p$164,p$165,p$166 -> [expansion from 1083] 1087 + p$164,~free(s,0)and beta(s,t) [expansion from 1083] 1088 + beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)) -> p$164 [expansion from 1083] 1089 + p$175,p$165 [expansion from 1084] 1090 + p$163,p$164 [expansion from 1087] 1091 + p$163 -> ~free(s,0) [expansion from 1087] 1092 + p$163 -> beta(s,t) [expansion from 1087] 1093 + p$163,free(s,0) -> [expansion from 1091] 1094 + p$162 -> p$164 [expansion from 1088] 1096 + ?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)) -> p$162 [expansion from 1088] 1097 + etas(abs(app(t,var(0))),A),beta(subst(s,0,u),A)or subst(s,0,u)=A -> p$162 [expansion from 1096] 1107 + p$164,beta(s,t) [negative chaining of 1090 from 1092] 1133 + p$160 -> p$165 [expansion from 1085] 1135 + ?A.(etas(abs(t),A)and(beta(abs(x),A)or abs(x)=A)) -> p$160 [expansion from 1085] 1136 + etas(abs(t),A),beta(abs(x),A)or abs(x)=A -> p$160 [expansion from 1135] 1242 + etas(t,A),beta(abs(x),abs(A))or abs(x)=abs(A) -> p$160 [negative chaining of 59 from 1136] 1349 + eta(t,A),beta(app(abs(s),x),subst(s,0,A))or app(abs(s),x)=subst(s,0,A) -> p$166 [negative chaining of 89 from 1082] 1409 + eta(abs(app(t,var(0))),A),beta(subst(s,0,u),A)or subst(s,0,u)=A -> p$162 [negative chaining of 38 from 1097] 1411 + eta(abs(app(t,var(0))),A),eta(A,B),beta(subst(s,0,u),B)or subst(s,0,u)=B -> p$162 [negative chaining of 198 from 1097] 1419 + beta(subst(s,0,u),A) -> p$153(A) [expansion from 1411] 1431 + beta(s,A) -> p$153(subst(A,0,u)) [negative chaining of 84 from 1419] 1436 + p$164,p$153(subst(t,0,u)) [negative chaining of 1107 from 1431] 1466 + beta(app(abs(s),x),subst(s,0,x))or app(abs(s),x)=subst(s,0,x) -> p$166,p$166 [negative chaining of 1079 from 1349] 1467 + beta(app(abs(s),x),subst(s,0,x))or app(abs(s),x)=subst(s,0,x) -> p$166 [condensement of 1466] 1468 + p$166 [reduction of 1467 by [26,L]] 1469 + p$164,p$165 -> [reduction of 1086 by [1468]] 1683 + beta(subst(s,0,u),subst(t,0,A))or subst(s,0,u)=subst(t,0,A) -> free(t,0),p$162 [negative chaining of 69 from 1409] 1698 + beta(subst(s,0,u),f$0(t,0))or subst(s,0,u)=f$0(t,0) -> p$162,free(t,0) [reduction of 1683 by [75,75]] 1700 + beta(subst(s,0,u),f$0(t,0))or subst(s,0,u)=f$0(t,0),beta(A,t) -> p$162,free(A,0) [negative chaining of 1698 from 81] 1705 + p$153(f$0(t,0)),beta(A,t) -> free(A,0),p$162 [expansion from 1700] 1786 + p$164,subst(t,A,B)=f$0(t,A),free(s,A),A<0 {[conj([free(t,A)>B],[],[])]} [negative chaining of 1107 from 486] 1865 + p$163 -> subst(t,0,A)=f$0(t,0),p$164 {[conj([free(s,0)>A],[],[])]} [negative chaining of 1786 from 1093] 1885 + p$164,subst(t,0,A)=f$0(t,0) {[conj([free(s,0)>A],[],[])]} [reduction of 1865 by [1090]] 1887 + p$153(f$0(t,0)),p$164,p$164 [chaining of 1885 from 1436] 1888 + p$153(f$0(t,0)),p$164 [condensement of 1887] 1893 + beta(A,t) -> p$164,free(A,0),p$162 [negative chaining of 1888 from 1705] 1898 + beta(A,t) -> p$164,free(A,0) [reduction of 1893 by [1094,L]] 1899 + beta(s,t),p$163 -> p$164 [negative chaining of 1898 from 1093] 1900 + p$164 [reduction of 1899 by [1107,1090]] 1901 + p$165 -> [reduction of 1469 by [1900]] 1902 + p$175 [reduction of 1089 by [1901,L]] 1903 + p$160 -> [reduction of 1133 by [1901,L]] 1904 + eta(s,x) [reduction of 874 by [1902]] 1905 + (beta(s,t)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t) [reduction of 873 by [1902,1904,L]] 1917 + etas(t,A),beta(abs(x),abs(A))or abs(x)=abs(A) -> [reduction of 1242 by [1903,L]] 1954 + beta(s,t)=>?A.(etas(t,A)and(beta(x,A)or x=A)) [expansion from 1905] 1955 + beta(s,t) [expansion from 1905] 1956 + beta(s,t) -> ?A.(etas(t,A)and(beta(x,A)or x=A)) [expansion from 1954] 1957 + beta(s,t) -> p$173 [expansion from 1956] 1958 + p$173 [reduction of 1957 by [1955]] 1959 + etas(t,s$3)and(beta(x,s$3)or x=s$3) [reduction of 901 by [1958]] 1960 + etas(t,s$3) [expansion from 1959] 1961 + beta(x,s$3)or x=s$3 [expansion from 1959] 1962 + beta(x,s$3),x=s$3 [expansion from 1961] 2050 + beta(abs(x),abs(s$3))or abs(x)=abs(s$3) -> [negative chaining of 1960 from 1917] 2053 + beta(abs(x),abs(s$3)) -> [expansion from 2050] 2055 + beta(x,s$3) -> [negative chaining of 29 from 2053] 2056 + s$3=x [reduction of 1962 by [2055,L]] 2057 + false [reduction of 1960 by [2056,1917,L,L,L]] Length = 228, Depth = 67 Total time: 1878240 milliseconds Number of forward inferences: 1297 Number of tableau inferences: 245 Number of kept clauses: 1294 */ /* 20021127 2.9.2 Proof: ====== 16 : subst(var(A),A,B)=B [input] 25 : subst(app(A,B),C,D)=app(subst(A,C,D),subst(B,C,D)) [input] 27 : eta(A,B) -> eta(abs(A),abs(B)) [input] 28 : eta(A,B) -> eta(app(A,C),app(B,C)) [input] 29 : eta(A,B) -> eta(app(C,A),app(C,B)) [input] 30 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0) [input] 31 : beta(app(abs(A),B),subst(A,0,B)) [input] 32 : beta(A,B) -> beta(app(C,A),app(C,B)) [input] 33 : beta(A,B) -> beta(app(A,C),app(B,C)) [input] 34 : beta(A,B) -> beta(abs(A),abs(B)) [input] 38 : etas(A,A) [input] 39 : eta(A,B) -> etas(A,B) [input] 47 : lemmaF1(A,B,C,D)==(~free(A,D)and 0=subst(A,D,B)=subst(A,D,C)) [input] 48 : comm_lemma(A,B,C)==(beta(A,B)and eta(A,C)=>?D.(etas(B,D)and betar(C,D))) [input] 49 : lemmaE2(A,B,C,D)==(0=eta(subst(A,D,C),subst(B,D,C))) [input] 50 : lemmaE7(A,B,C,D)==(0=etas(subst(C,D,A),subst(C,D,B))) [input] 51 : lemmaB1(A,B,C)==(0=beta(A,B)=>free(B,C)=>free(A,C)) [input] 52 : lemmaB2(A,B,C,D)==(0=beta(A,B)=>beta(subst(A,D,C),subst(B,D,C))) [input] 53 : lemmaE7(A,B,C,D) [input] 54 : lemmaF1(A,B,C,D) [input] 55 : lemmaE2(A,B,C,D) [input] 56 : lemmaB1(A,B,C) [input] 57 : lemmaB2(A,B,C,D) [input] 58 : etas(A,B) -> etas(app(A,C),app(B,C)) [input] 59 : etas(A,B) -> etas(app(C,A),app(C,B)) [input] 60 : etas(A,B) -> etas(abs(A),abs(B)) [input] 61 : betar(A,B)==(beta(A,B)or A=B) [input] 62 + ~free(s,0)=>comm_lemma(app(abs(app(s,var(0))),t),subst(app(s,var(0)),0,t),app(subst(s,0,u),t)),eta(s,t)=>comm_lemma(app(abs(s),u),subst(s,0,u),app(abs(t),u)),eta(t,x)=>comm_lemma(app(abs(s),t),subst(s,0,t),app(abs(s),x)),comm_lemma(s,t,x)and beta(s,t)and eta(s,x)=>comm_lemma(abs(s),abs(t),abs(x)),~free(s,0)and beta(s,t)=>comm_lemma(abs(app(s,var(0))),abs(app(t,var(0))),subst(s,0,u)),comm_lemma(s,t,x)and beta(s,t)and eta(s,x)and eta(u,v)=>comm_lemma(app(s,u),app(t,u),app(x,u))and comm_lemma(app(u,s),app(u,t),app(u,x))and comm_lemma(app(s,u),app(t,u),app(s,v))and comm_lemma(app(u,s),app(u,t),app(v,s)) -> [input] 64 : 0=etas(subst(D,A,B),subst(D,A,C)) [reduction of 53 by [50]] 65 : 0= etas(subst(D,A,B),subst(D,A,C)) [condensement of 64] 66 : ~free(A,B)and 0=subst(A,B,C)=subst(A,B,D) [reduction of 54 by [47]] 67 : ~free(A,B),0= subst(A,B,C)=subst(A,B,D) [condensement of 66] 68 : 0= subst(B,A,C)=subst(B,A,D),free(B,A) [reduction of 67 by [L]] 69 : 0= subst(B,A,C)=f$0(B,A),free(B,A) [variable elimination from 68] 70 : A<0,subst(B,A,C)=f$0(B,A),free(B,A) [totality resolution from 69] 71 : 0= subst(B,A,C)=f$0(B,A),free(B,A) [variable elimination from 68] 72 : A<0,subst(B,A,C)=f$0(B,A),free(B,A) [totality resolution from 71] 73 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 55 by [49]] 74 : 0= eta(subst(B,A,D),subst(C,A,D)) [condensement of 73] 75 : 0=beta(B,C)=>free(C,A)=>free(B,A) [reduction of 56 by [51]] 76 : free(A,B),beta(C,A),0= free(C,B) [condensement of 75] 77 : 0=beta(B,C)=>beta(subst(B,A,D),subst(C,A,D)) [reduction of 57 by [52]] 78 : beta(A,B),0= beta(subst(A,C,D),subst(B,C,D)) [condensement of 77] 79 + ~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs( 67 : ~free(A,B),0= subst(A,B,C)=subst(A,B,D) [condensement of 66] 68 : 0= subst(B,A,C)=subst(B,A,D),free(B,A) [reduction of 67 by [L]] 69 : 0= subst(B,A,C)=f$0(B,A),free(B,A) [variable elimination from 68] 70 : A<0,subst(B,A,C)=f$0(B,A),free(B,A) [totality resolution from 69] 71 : 0= subst(B,A,C)=f$0(B,A),free(B,A) [variable elimination from 68] 72 : A<0,subst(B,A,C)=f$0(B,A),free(B,A) [totality resolution from 71] 73 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 55 by [49]] 74 : 0= eta(subst(B,A,D),subst(C,A,D)) [condensement of 73] 75 : 0=beta(B,C)=>free(C,A)=>free(B,A) [reduction of 56 by [51]] 76 : free(A,B),beta(C,A),0= free(C,B) [condensement of 75] 77 : 0=beta(B,C)=>beta(subst(B,A,D),subst(C,A,D)) [reduction of 57 by [52]] 78 : beta(A,B),0= beta(subst(A,C,D),subst(B,C,D)) [condensement of 77] 79 + ~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)),(beta(s,t)and eta(s,x)=>?B.(etas(t,B)and(beta(x,B)or x=B)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?C.(etas(abs(t),C)and(beta(abs(x),C)or abs(x)=C)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?D.(etas(subst(s,0,t),D)and(beta(app(abs(s),x),D)or app(abs(s),x)=D)),eta(s,t)=>eta(app(abs(s),u),app(abs(t),u))=>?E.(etas(subst(s,0,u),E)and(beta(app(abs(t),u),E)or app(abs(t),u)=E)),~free(s,0)=>beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?F.(etas(app(subst(s,0,t),t),F)and(beta(app(subst(s,0,u),t),F)or app(subst(s,0,u),t)=F)),(beta(s,t)and eta(s,x)=>?G.(etas(t,G)and(beta(x,G)or x=G)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?H.(etas(app(t,u),H)and(beta(app(x,u),H)or app(x,u)=H)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?I.(etas(app(u,t),I)and(beta(app(u,x),I)or app(u,x)=I)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?J.(etas(app(t,u),J)and(beta(app(s,v),J)or app(s,v)=J)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?K.(etas(app(u,t),K)and(beta(app(v,s),K)or app(v,s)=K))) -> [reduction of 62 by [25,16,48,61,48,61,31,L,48,61,31,L,48,61,48,61,48,61,48,61,48,61,48,61,48,61,48,61]] 80 : free(A,0),eta(abs(app(A,var(0))),f$0(A,0)) [reduction of 30 by [72]] 82 : eta(A,B) -> etas(subst(C,0,A),subst(C,0,B)) [reflexivity resolution from 65] 83 : eta(A,B) -> eta(subst(A,0,C),subst(B,0,C)) [reflexivity resolution from 74] 84 : beta(A,B),free(B,0) -> free(A,0) [reflexivity resolution from 76] 85 : beta(A,B) -> beta(subst(A,0,C),subst(B,0,C)) [reflexivity resolution from 78] 86 + q$499,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?B.(etas(abs(t),B)and(beta(abs(x),B)or abs(x)=B)),(beta(s,t)and eta(s,x)=>?C.(etas(t,C)and(beta(x,C)or x=C)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?D.(etas(app(t,u),D)and(beta(app(x,u),D)or app(x,u)=D)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?E.(etas(app(u,t),E)and(beta(app(u,x),E)or app(u,x)=E)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?F.(etas(app(t,u),F)and(beta(app(s,v),F)or app(s,v)=F)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?G.(etas(app(u,t),G)and(beta(app(v,s),G)or app(v,s)=G))),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?H.(etas(abs(app(t,var(0))),H)and(beta(subst(s,0,u),H)or subst(s,0,u)=H)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?I.(etas(subst(s,0,t),I)and(beta(app(abs(s),x),I)or app(abs(s),x)=I)),~free(s,0)=>beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?J.(etas(app(subst(s,0,t),t),J)and(beta(app(subst(s,0,u),t),J)or app(subst(s,0,u),t)=J)) -> [expansion from 79] 87 + q$499,eta(s,t) [expansion from 79] 88 + eta(app(abs(s),u),app(abs(t),u))=>?A.(etas(subst(s,0,u),A)and(beta(app(abs(t),u),A)or app(abs(t),u)=A)) -> q$499 [expansion from 79] 89 + ?A.(etas(subst(s,0,u),A)and(beta(app(abs(t),u),A)or app(abs(t),u)=A)) -> q$499 [reduction of 88 by [28,27,87,L]] 90 + etas(subst(s,0,u),A),beta(app(abs(t),u),A)or app(abs(t),u)=A -> q$499 [condensement of 89] 91 + q$498,q$499,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.(etas(app(u,t),C)and(beta(app(u,x),C)or app(u,x)=C)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?D.(etas(app(t,u),D)and(beta(app(s,v),D)or app(s,v)=D)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?E.(etas(app(u,t),E)and(beta(app(v,s),E)or app(v,s)=E))),(beta(s,t)and eta(s,x)=>?F.(etas(t,F)and(beta(x,F)or x=F)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?G.(etas(abs(t),G)and(beta(abs(x),G)or abs(x)=G)),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?H.(etas(abs(app(t,var(0))),H)and(beta(subst(s,0,u),H)or subst(s,0,u)=H)),eta(t,x)=>eta(app(abs(s),t),app(abs(s),x))=>?I.(etas(subst(s,0,t),I)and(beta(app(abs(s),x),I)or app(abs(s),x)=I)) -> [expansion from 86] 92 + q$498,~free(s,0) [expansion from 86] 93 + beta(app(abs(app(s,var(0))),t),app(subst(s,0,t),t))and eta(app(abs(app(s,var(0))),t),app(subst(s,0,u),t))=>?A.(etas(app(subst(s,0,t),t),A)and(beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A)) -> q$498 [expansion from 86] 94 + free(s,0) -> q$498 [reduction of 92 by [L]] 95 + etas(subst(s,0,u),A),beta(app(abs(t),u),A) -> q$499 [expansion from 90] 97 + q$497,q$498,q$499,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.(etas(app(u,t),C)and(beta(app(u,x),C)or app(u,x)=C)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?D.(etas(app(t,u),D)and(beta(app(s,v),D)or app(s,v)=D)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?E.(etas(app(u,t),E)and(beta(app(v,s),E)or app(v,s)=E))),(beta(s,t)and eta(s,x)=>?F.(etas(t,F)and(beta(x,F)or x=F)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?G.(etas(abs(t),G)and(beta(abs(x),G)or abs(x)=G)),~free(s,0)and beta(s,t)=>beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?H.(etas(abs(app(t,var(0))),H)and(beta(subst(s,0,u),H)or subst(s,0,u)=H)) -> [expansion from 91] 98 + q$497,eta(t,x) [expansion from 91] 99 + eta(app(abs(s),t),app(abs(s),x))=>?A.(etas(subst(s,0,t),A)and(beta(app(abs(s),x),A)or app(abs(s),x)=A)) -> q$497 [expansion from 91] 100 + ?A.(etas(subst(s,0,t),A)and(beta(app(abs(s),x),A)or app(abs(s),x)=A)) -> q$497 [reduction of 99 by [29,98,L]] 101 + etas(subst(s,0,t),A),beta(app(abs(s),x),A)or app(abs(s),x)=A -> q$497 [condensement of 100] 103 + etas(app(subst(s,0,t),t),A),beta(app(subst(s,0,u),t),A)or app(subst(s,0,u),t)=A -> q$498 [expansion from 93] 105 + q$496,q$497,q$498,q$499,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.(etas(app(u,t),C)and(beta(app(u,x),C)or app(u,x)=C)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?D.(etas(app(t,u),D)and(beta(app(s,v),D)or app(s,v)=D)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?E.(etas(app(u,t),E)and(beta(app(v,s),E)or app(v,s)=E))),(beta(s,t)and eta(s,x)=>?F.(etas(t,F)and(beta(x,F)or x=F)))and beta(s,t)and eta(s,x)=>beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?G.(etas(abs(t),G)and(beta(abs(x),G)or abs(x)=G)) -> [expansion from 97] 106 + q$496,~free(s,0)and beta(s,t) [expansion from 97] 107 + beta(abs(app(s,var(0))),abs(app(t,var(0))))and eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(etas(abs(app(t,var(0))),A)and(beta(subst(s,0,u),A)or subst(s,0,u)=A)) -> q$496 [expansion from 97] 108 + etas(subst(s,0,t),A),beta(app(abs(s),x),A) -> q$497 [expansion from 101] 113 + etas(app(subst(s,0,t),t),A),app(subst(s,0,u),t)=A -> q$498 [expansion from 103] 114 + q$495,q$496,q$497,q$498,q$499,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)and eta(u,v)=>(beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.(etas(app(u,t),C)and(beta(app(u,x),C)or app(u,x)=C)))and(beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?D.(etas(app(t,u),D)and(beta(app(s,v),D)or app(s,v)=D)))and(beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?E.(etas(app(u,t),E)and(beta(app(v,s),E)or app(v,s)=E))) -> [expansion from 105] 115 + q$495,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x) [expansion from 105] 116 + beta(abs(s),abs(t))and eta(abs(s),abs(x))=>?A.(etas(abs(t),A)and(beta(abs(x),A)or abs(x)=A)) -> q$495 [expansion from 105] 117 + q$496,~free(s,0) [expansion from 106] 118 + q$496,beta(s,t) [expansion from 106] 120 + etas(abs(app(t,var(0))),A),beta(subst(s,0,u),A)or subst(s,0,u)=A -> q$496 [expansion from 107] 122 + etas(app(subst(s,0,t),t),app(subst(s,0,u),t)) -> q$498 [reflexivity resolution from 113] 123 + q$495,q$496,q$497,q$498,q$499 -> (beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x)and eta(u,v) [expansion from 114] 124 + beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?A.(etas(app(t,u),A)and(beta(app(x,u),A)or app(x,u)=A)),beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?B.(etas(app(u,t),B)and(beta(app(u,x),B)or app(u,x)=B)),beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?C.(etas(app(t,u),C)and(beta(app(s,v),C)or app(s,v)=C)),beta(app(u,s),app(u,t))and eta(app(u,s),app(v,s))=>?D.(etas(app(u,t),D)and(beta(app(v,s),D)or app(v,s)=D)),q$495,q$496,q$497,q$498,q$499 -> [expansion from 114] 125 + q$495,(beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t) [expansion from 115] 126 + q$495,eta(s,x) [expansion from 115] 128 + etas(abs(t),A),beta(abs(x),A)or abs(x)=A -> q$495 [expansion from 116] 132 + eta(subst(s,0,u),A),beta(app(abs(t),u),A) -> q$499 [negative chaining of 39 from 95] 134 + free(s,0) -> q$496 [reduction of 117 by [L]] 137 + etas(abs(app(t,var(0))),A),beta(subst(s,0,u),A) -> q$496 [expansion from 120] 139 + q$495,q$496,q$497,q$498,q$499 -> (beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t)and eta(s,x) [expansion from 123] 140 + q$495,q$496,q$497,q$498,q$499 -> eta(u,v) [expansion from 123] 141 + q$494,beta(app(s,u),app(t,u))and eta(app(s,u),app(s,v))=>?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)),q$495,q$496,q$497,q$498,q$499,beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)),beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.(etas(app(u,t),C)and(beta(app(u,x),C)or app(u,x)=C)) -> [expansion from 124] 143 + etas(app(u,t),A),beta(app(v,s),A)or app(v,s)=A -> q$494 [expansion from 124] 144 + q$494,beta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?A.(etas(app(u,t),A)and(beta(app(u,x),A)or app(u,x)=A)),beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)),q$499,q$498,q$497,q$496,q$495,beta(app(s,u),app(t,u))=>?C.(etas(app(t,u),C)and(beta(app(s,v),C)or app(s,v)=C)) -> [reduction of 141 by [29,140,L]] 145 + beta(s,t),eta(s,x) -> ?A.(etas(t,A)and(beta(x,A)or x=A)),q$495 [expansion from 125] 146 + q$495,beta(s,t) [expansion from 125] 147 + etas(abs(t),A),beta(abs(x),A) -> q$495 [expansion from 128] 148 + etas(abs(t),A),abs(x)=A -> q$495 [expansion from 128] 150 + q$495,q$496,q$497,q$498,q$499 -> (beta(s,t)and eta(s,x)=>?A.(etas(t,A)and(beta(x,A)or x=A)))and beta(s,t) [expansion from 139] 151 + q$495,q$496,q$497,q$498,q$499 -> eta(s,x) [expansion from 139] 152 + q$493,q$494,beta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?A.(etas(app(t,u),A)and(beta(app(x,u),A)or app(x,u)=A)),q$499,q$498,q$497,q$496,q$495,beta(app(s,u),app(t,u))=>?B.(etas(app(t,u),B)and(beta(app(s,v),B)or app(s,v)=B)) -> [expansion from 144] 154 + etas(app(u,t),A),beta(app(u,x),A)or app(u,x)=A -> q$493 [expansion from 144] 155 + beta(s,t) -> q$495,?A.(etas(t,A)and(beta(x,A)or x=A)) [reduction of 145 by [126]] 156 + q$499,q$498,q$497,q$496 -> eta(s,x) [reduction of 151 by [126]] 157 + q$493,q$494,beta(app(s,u),app(t,u))=>?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)),q$495,q$496,q$497,q$498,q$499,beta(app(s,u),app(t,u))=>?B.(etas(app(t,u),B)and(beta(app(x,u),B)or app(x,u)=B)) -> [reduction of 152 by [28,156,L]] 160 + etas(app(u,t),A),beta(app(v,s),A) -> q$494 [expansion from 143] 162 + beta(s,t) -> q$495,etas(t,s$2)and(beta(x,s$2)or x=s$2) [expansion from 155] 164 + etas(abs(t),abs(x)) -> q$495 [reflexivity resolution from 148] 165 + beta(s,t),eta(s,x),q$495,q$496,q$497,q$498,q$499 -> ?A.(etas(t,A)and(beta(x,A)or x=A)) [expansion from 150] 166 + q$495,q$496,q$497,q$498,q$499 -> beta(s,t) [expansion from 150] 167 + q$492,q$493,q$494,q$495,q$496,q$497,q$498,q$499,beta(app(s,u),app(t,u))=>?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)) -> [expansion from 157] 169 + etas(app(t,u),A),beta(app(x,u),A)or app(x,u)=A -> q$492 [expansion from 157] 170 + etas(t,s$2)and(beta(x,s$2)or x=s$2),q$495 [reduction of 162 by [146]] 172 + beta(s,t),q$499,q$498,q$497,q$496,q$495 -> ?A.(etas(t,A)and(beta(x,A)or x=A)) [reduction of 165 by [156]] 173 + q$499,q$498,q$497 -> beta(s,t) [reduction of 166 by [146,118]] 174 + q$492,q$493,q$494,q$495,q$496,q$497,q$498,q$499,?A.(etas(app(t,u),A)and(beta(app(s,v),A)or app(s,v)=A)) -> [reduction of 167 by [33,173,L]] 175 + etas(app(t,u),A),beta(app(s,v),A)or app(s,v)=A,q$492,q$493,q$494,q$495,q$496,q$497,q$498,q$499 -> [condensement of 174] 178 + etas(app(u,t),A),beta(app(u,x),A) -> q$493 [expansion from 154] 179 + etas(app(u,t),A),app(u,x)=A -> q$493 [expansion from 154] 181 + q$495,etas(t,s$2) [expansion from 170] 182 + beta(x,s$2),x=s$2,q$495 [expansion from 170] 183 + q$499,q$498,q$497,q$496,q$495,beta(s,t) -> etas(t,s$3)and(beta(x,s$3)or x=s$3) [expansion from 172] 185 + q$499,q$498,q$497,q$496,q$495,q$494,q$493,q$492,etas(app(t,u),A),beta(app(s,v),A) -> [expansion from 175] 187 + etas(app(t,u),A),beta(app(x,u),A) -> q$492 [expansion from 169] 188 + etas(app(t,u),A),app(x,u)=A -> q$492 [expansion from 169] 200 + eta(abs(app(t,var(0))),A),beta(subst(s,0,u),A) -> q$496 [negative chaining of 39 from 137] 202 + q$499,q$498,q$497,q$496,q$495 -> etas(t,s$3)and(beta(x,s$3)or x=s$3) [reduction of 183 by [173]] 204 + etas(app(u,t),app(u,x)) -> q$493 [reflexivity resolution from 179] 205 + q$498,q$497,q$496,q$495,q$499 -> etas(t,s$3) [expansion from 202] 206 + q$498,q$497,q$496,q$495,q$499 -> beta(x,s$3),x=s$3 [expansion from 202] 207 + etas(app(t,u),app(x,u)) -> q$492 [reflexivity resolution from 188] 213 + free(t,0) -> q$496,free(s,0) [negative chaining of 118 from 84] 218 + q$498,q$497,q$499,free(t,0) -> free(s,0) [negative chaining of 173 from 84] 222 + free(t,0) -> q$496 [reduction of 213 by [134,L]] 241 + etas(t,x) -> q$495 [negative chaining of 60 from 164] 242 + etas(t,A),beta(abs(x),abs(A)) -> q$495 [negative chaining of 60 from 147] 249 + beta(abs(x),abs(s$2)) -> q$495,q$495 [negative chaining of 181 from 242] 250 + beta(abs(x),abs(s$2)) -> q$495 [condensement of 249] 252 + beta(x,s$2) -> q$495 [negative chaining of 34 from 250] 273 + s$2=x,q$495,q$495 [negative chaining of 182 from 252] 279 + s$2=x,q$495 [condensement of 273] 285 + etas(t,x),q$495,q$495 [chaining of 279 from 181] 290 + etas(t,x),q$495 [condensement of 285] 291 + q$495 [reduction of 290 by [241,L]] 295 + q$499,q$498,q$497,q$496 -> eta(u,v) [reduction of 140 by [291]] 296 + q$499,q$492,q$493,q$494,etas(app(t,u),A),beta(app(s,v),A),q$498,q$497,q$496 -> [reduction of 185 by [291]] 299 + q$497,q$496,q$499,q$498 -> etas(t,s$3) [reduction of 205 by [291]] 300 + q$497,q$496,q$499,q$498 -> s$3=x,beta(x,s$3) [reduction of 206 by [291]] 305 + subst(s,0,A)=f$0(s,0),q$498 {[conj([free(s,0)>A],[],[])]} [negative chaining of 70 from 94] 310 + subst(s,0,A)=f$0(s,0),q$496 {[conj([free(s,0)>A],[],[])]} [negative chaining of 70 from 134] 312 + subst(t,0,A)=f$0(t,0),q$496 {[conj([free(t,0)>A],[],[])]} [negative chaining of 70 from 222] 361 + etas(app(subst(s,0,t),t),app(f$0(s,0),t)) -> q$498,q$498 [negative chaining of 305 from 122] 373 + etas(app(subst(s,0,t),t),app(f$0(s,0),t)) -> q$498 [condensement of 361] 374 + q$498 [reduction of 373 by [305,38]] 378 + q$499,q$497 -> beta(s,t) [reduction of 173 by [374]] 380 + free(t,0),q$497,q$499 -> free(s,0) [reduction of 218 by [374]] 381 + q$499,q$496,q$497,etas(app(t,u),A),beta(app(s,v),A),q$492,q$493,q$494 -> [reduction of 296 by [374]] 385 + q$499,q$496,q$497 -> eta(u,v) [reduction of 295 by [374]] 387 + q$496,q$497,q$499 -> etas(t,s$3) [reduction of 299 by [374]] 388 + q$496,q$497,q$499 -> s$3=x,beta(x,s$3) [reduction of 300 by [374]] 417 + eta(t,A),beta(app(abs(s),x),subst(s,0,A)) -> q$497 [negative chaining of 82 from 108] 459 + beta(s,A) -> beta(f$0(s,0),subst(A,0,B)),q$496 {[conj([free(s,0)>B],[],[])]} [chaining of 310 from 85] 466 + etas(u,A),beta(app(v,s),app(A,t)) -> q$494 [negative chaining of 58 from 160] 468 + etas(t,A),beta(app(x,u),app(A,u)) -> q$492 [negative chaining of 58 from 187] 469 + etas(t,x) -> q$492 [negative chaining of 58 from 207] 473 + eta(u,A),beta(app(v,s),app(A,t)) -> q$494 [negative chaining of 39 from 466] 478 + q$496,q$497,q$499,beta(app(x,u),app(s$3,u)) -> q$492 [negative chaining of 387 from 468] 480 + q$496,q$497,q$499,beta(app(v,s),app(v,t)) -> q$494 [negative chaining of 385 from 473] 484 + etas(t,A),beta(app(u,x),app(u,A)) -> q$493 [negative chaining of 59 from 178] 486 + etas(t,x) -> q$493 [negative chaining of 59 from 204] 488 + q$496,q$497,q$499 -> q$494 [reduction of 480 by [32,378]] 489 + eta(t,x) -> q$493 [negative chaining of 39 from 486] 493 + q$497,q$493 [negative chaining of 98 from 489] 496 + q$496,q$497,q$499,beta(app(u,x),app(u,s$3)) -> q$493 [negative chaining of 387 from 484] 497 + q$496,beta(app(u,x),app(u,s$3)),q$499 -> q$493 [reduction of 496 by [493]] 560 + beta(s,t) -> beta(f$0(s,0),f$0(t,0)),q$496,q$496 {[conj([free(s,0)>A],[],[])]} [chaining of 312 from 459] 564 + beta(s,t) -> beta(f$0(s,0),f$0(t,0)),q$496 {[conj([free(s,0)>A],[],[])]} [condensement of 560] 565 + q$496,beta(f$0(s,0),f$0(t,0)) {[conj([free(s,0)>A],[],[])]} [reduction of 564 by [118]] 567 + beta(x,s$3),q$496,q$499 -> q$493 [negative chaining of 32 from 497] 572 + q$496,q$497,q$499,q$496,q$499 -> s$3=x,q$493 [negative chaining of 388 from 567] 589 + q$497,q$496,q$499 -> s$3=x,q$493 [condensement of 572] 590 + q$499,q$496 -> q$493,s$3=x [reduction of 589 by [493]] 595 + q$496,q$499,q$496,q$497,q$499 -> etas(t,x),q$493 [chaining of 590 from 387] 598 + q$496,q$497,q$499 -> etas(t,x),q$493 [condensement of 595] 599 + q$499,q$496 -> q$493 [reduction of 598 by [493,486,L]] 604 + eta(s,A),beta(app(abs(t),u),subst(A,0,u)) -> q$499 [negative chaining of 83 from 132] 610 + beta(app(abs(s),x),subst(s,0,x)) -> q$497,q$497 [negative chaining of 98 from 417] 611 + beta(app(abs(t),u),subst(t,0,u)) -> q$499,q$499 [negative chaining of 87 from 604] 619 + beta(app(abs(s),x),subst(s,0,x)) -> q$497 [condensement of 610] 620 + q$497 [reduction of 619 by [31]] 621 + beta(app(abs(t),u),subst(t,0,u)) -> q$499 [condensement of 611] 622 + q$499 [reduction of 621 by [31]] 626 + beta(s,t) [reduction of 378 by [620,622]] 628 + q$496 -> eta(u,v) [reduction of 385 by [620,622]] 630 + q$496 -> etas(t,s$3) [reduction of 387 by [620,622]] 631 + q$496 -> s$3=x,beta(x,s$3) [reduction of 388 by [620,622]] 632 + free(t,0) -> free(s,0) [reduction of 380 by [620,622]] 635 + beta(app(x,u),app(s$3,u)),q$496 -> q$492 [reduction of 478 by [620,622]] 637 + q$496 -> q$494 [reduction of 488 by [622,620]] 638 + q$493,q$492,etas(app(t,u),A),beta(app(s,v),A),q$496 -> [reduction of 381 by [622,637,620]] 644 + q$496 -> q$493 [reduction of 599 by [622]] 671 + beta(x,s$3),q$496 -> q$492 [negative chaining of 33 from 635] 685 + q$496,q$496 -> s$3=x,q$492 [negative chaining of 631 from 671] 691 + q$496 -> s$3=x,q$492 [condensement of 685] 696 + q$496,q$496 -> etas(t,x),q$492 [chaining of 691 from 630] 701 + q$496 -> etas(t,x),q$492 [condensement of 696] 702 + q$496 -> q$492 [reduction of 701 by [469,L]] 709 + beta(subst(s,0,u),f$0(t,0)) -> free(t,0),q$496 [negative chaining of 80 from 200] 720 + q$496 [reduction of 709 by [310,565,632,134,L,L]] 722 + eta(u,v) [reduction of 628 by [720]] 726 + q$493 [reduction of 644 by [720]] 729 + etas(app(t,u),A),beta(app(s,v),A),q$492 -> [reduction of 638 by [720,726]] 737 + q$492 [reduction of 702 by [720]] 739 + etas(app(t,u),A),beta(app(s,v),A) -> [reduction of 729 by [737]] 745 + eta(app(t,u),A),beta(app(s,v),A) -> [negative chaining of 39 from 739] 760 + eta(u,A),beta(app(s,v),app(t,A)) -> [negative chaining of 29 from 745] 769 + beta(app(s,v),app(t,v)) -> [negative chaining of 722 from 760] 780 + false [reduction of 769 by [33,626]] Length = 214, Depth = 40, Search Depth = 3 Total time: 88358 milliseconds Number of forward inferences: 432 Number of tableau inferences: 81 Number of generated clauses: 780 Number of kept clauses: 437 */