use(subst). use(beta). use(eta). 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(2)]). :-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 */