use(subst). use(int). use(eta). use(lemmaE8). use(lemmaE2). use(lemmaE1). lemmaE1(S,T,I). lemmaE2(S,T,U,I). goal %Induktionsanfang der Induktion ueber eta (~free(s,0) => lemmaE8(abs(app(s,var(0))),subst(s,0,u),subst(s,0,u))), ((~free(s,0) and eta(s,t)) => lemmaE8(abs(app(s,var(0))),subst(s,0,u),abs(app(t,var(0))))), %1. Induktionsschritt (eta(s,t) => ( ((eta(s,x) and lemmaE8(s,t,x)) => (lemmaE8(app(s,u),app(t,u),app(x,u)) and lemmaE8(app(u,s),app(u,t),app(u,x)))) and (eta(a,b) => (lemmaE8(app(s,a),app(t,a),app(s,b)) and lemmaE8(app(a,s),app(a,t),app(b,s)))) )), %2. Induktionsschritt ((eta(s,t) and eta(s,x) and lemmaE8(s,t,x)) => lemmaE8(abs(s),abs(t),abs(x))) -> []. top_predicates_precedence([lemmaE8,lemmaE1,lemmaE2]). option([var_overlaps(off),search_depth(3)]). :-sarp(+[15]),saci([2]). /* Proof: ====== 39 : ~free(A,0) -> eta(abs(app(A,var(0))),subst(A,0,B)) [input] 40 : eta(A,B) -> eta(app(A,C),app(B,C)) [input] 41 : eta(A,B) -> eta(app(C,A),app(C,B)) [input] 42 : eta(A,B) -> eta(abs(A),abs(B)) [input] 46 : lemmaE8(A,B,C)==(eta(A,B)and eta(A,C)=>?D.((D=B or eta(B,D))and(D=C or eta(C,D)))) [input] 47 : lemmaE2(A,B,C,D)==(0=eta(subst(A,D,C),subst(B,D,C))) [input] 48 : lemmaE1(A,B,C)==(0=free(B,C)<=>free(A,C)) [input] 49 : lemmaE1(A,B,C) [input] 50 : lemmaE2(A,B,C,D) [input] 51 + ~free(s,0)=>lemmaE8(abs(app(s,var(0))),subst(s,0,u),subst(s,0,u)),~free(s,0)and eta(s,t)=>lemmaE8(abs(app(s,var(0))),subst(s,0,u),abs(app(t,var(0)))),eta(s,t)=>(eta(s,x)and lemmaE8(s,t,x)=>lemmaE8(app(s,u),app(t,u),app(x,u))and lemmaE8(app(u,s),app(u,t),app(u,x)))and(eta(a,b)=>lemmaE8(app(s,a),app(t,a),app(s,b))and lemmaE8(app(a,s),app(a,t),app(b,s))),eta(s,t)and eta(s,x)and lemmaE8(s,t,x)=>lemmaE8(abs(s),abs(t),abs(x)) -> [input] 62 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0) [expansion from 39] 64 : 0=free(C,A)<=>free(B,A) [reduction of 49 by [48]] 65 : 0= free(C,A)==free(B,A) [expansion from 64] 66 : eta(A,B) -> C<0,free(B,C)==free(A,C) [totality resolution from 65] 67 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 50 by [47]] 68 : 0= eta(subst(B,A,D),subst(C,A,D)) [expansion from 67] 69 : eta(A,B) -> C<0,eta(subst(A,C,D),subst(B,C,D)) [totality resolution from 68] 70 + eta(s,t)=>(eta(s,x)and(eta(s,t)and eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))))=>(eta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.((B=app(t,u)or eta(app(t,u),B))and(B=app(x,u)or eta(app(x,u),B))))and(eta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.((C=app(u,t)or eta(app(u,t),C))and(C=app(u,x)or eta(app(u,x),C)))))and(eta(a,b)=>(eta(app(s,a),app(t,a))and eta(app(s,a),app(s,b))=>?D.((D=app(t,a)or eta(app(t,a),D))and(D=app(s,b)or eta(app(s,b),D))))and(eta(app(a,s),app(a,t))and eta(app(a,s),app(b,s))=>?E.((E=app(a,t)or eta(app(a,t),E))and(E=app(b,s)or eta(app(b,s),E))))),~free(s,0)and eta(s,t)=>eta(abs(app(s,var(0))),subst(s,0,u))and eta(abs(app(s,var(0))),abs(app(t,var(0))))=>?F.((F=subst(s,0,u)or eta(subst(s,0,u),F))and(F=abs(app(t,var(0)))or eta(abs(app(t,var(0))),F))),~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?G.(G=subst(s,0,u)or eta(subst(s,0,u),G)),eta(s,t)and eta(s,x)and(eta(s,t)and eta(s,x)=>?H.((H=t or eta(t,H))and(H=x or eta(x,H))))=>eta(abs(s),abs(t))and eta(abs(s),abs(x))=>?I.((I=abs(t)or eta(abs(t),I))and(I=abs(x)or eta(abs(x),I))) -> [reduction of 51 by [46,L,L,46,46,46,46,46,46,46,46]] 71 + p$199,eta(s,t)and eta(s,x)and(eta(s,t)and eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))))=>eta(abs(s),abs(t))and eta(abs(s),abs(x))=>?B.((B=abs(t)or eta(abs(t),B))and(B=abs(x)or eta(abs(x),B))),~free(s,0)and eta(s,t)=>eta(abs(app(s,var(0))),subst(s,0,u))and eta(abs(app(s,var(0))),abs(app(t,var(0))))=>?C.((C=subst(s,0,u)or eta(subst(s,0,u),C))and(C=abs(app(t,var(0)))or eta(abs(app(t,var(0))),C))),~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?D.(D=subst(s,0,u)or eta(subst(s,0,u),D)) -> [expansion from 70] 72 + p$199,eta(s,t) [expansion from 70] 73 + (eta(s,x)and(eta(s,t)and eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))))=>(eta(app(s,u),app(t,u))and eta(app(s,u),app(x,u))=>?B.((B=app(t,u)or eta(app(t,u),B))and(B=app(x,u)or eta(app(x,u),B))))and(eta(app(u,s),app(u,t))and eta(app(u,s),app(u,x))=>?C.((C=app(u,t)or eta(app(u,t),C))and(C=app(u,x)or eta(app(u,x),C)))))and(eta(a,b)=>(eta(app(s,a),app(t,a))and eta(app(s,a),app(s,b))=>?D.((D=app(t,a)or eta(app(t,a),D))and(D=app(s,b)or eta(app(s,b),D))))and(eta(app(a,s),app(a,t))and eta(app(a,s),app(b,s))=>?E.((E=app(a,t)or eta(app(a,t),E))and(E=app(b,s)or eta(app(b,s),E))))) -> p$199 [expansion from 70] 74 + (eta(s,x)and(eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))))=>(eta(app(s,u),app(x,u))=>?B.((B=app(t,u)or eta(app(t,u),B))and(B=app(x,u)or eta(app(x,u),B))))and(eta(app(u,s),app(u,x))=>?C.((C=app(u,t)or eta(app(u,t),C))and(C=app(u,x)or eta(app(u,x),C)))))and(eta(a,b)=>(eta(app(s,a),app(s,b))=>?D.((D=app(t,a)or eta(app(t,a),D))and(D=app(s,b)or eta(app(s,b),D))))and(eta(app(a,s),app(b,s))=>?E.((E=app(a,t)or eta(app(a,t),E))and(E=app(b,s)or eta(app(b,s),E))))) -> p$199 [reduction of 73 by [41,72,L,40,72,L,41,72,L,40,72,L,72,L]] 75 + eta(s,x)and(eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))))=>(eta(app(s,u),app(x,u))=>?B.((B=app(t,u)or eta(app(t,u),B))and(B=app(x,u)or eta(app(x,u),B))))and(eta(app(u,s),app(u,x))=>?C.((C=app(u,t)or eta(app(u,t),C))and(C=app(u,x)or eta(app(u,x),C)))),eta(a,b)=>(eta(app(s,a),app(s,b))=>?D.((D=app(t,a)or eta(app(t,a),D))and(D=app(s,b)or eta(app(s,b),D))))and(eta(app(a,s),app(b,s))=>?E.((E=app(a,t)or eta(app(a,t),E))and(E=app(b,s)or eta(app(b,s),E)))) -> p$199 [expansion from 74] 76 + p$198,~free(s,0)and eta(s,t)=>eta(abs(app(s,var(0))),subst(s,0,u))and eta(abs(app(s,var(0))),abs(app(t,var(0))))=>?A.((A=subst(s,0,u)or eta(subst(s,0,u),A))and(A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A))),~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?B.(B=subst(s,0,u)or eta(subst(s,0,u),B)),p$199 -> [expansion from 71] 77 + p$198,eta(s,t)and eta(s,x)and(eta(s,t)and eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A)))) [expansion from 71] 78 + eta(abs(s),abs(t))and eta(abs(s),abs(x))=>?A.((A=abs(t)or eta(abs(t),A))and(A=abs(x)or eta(abs(x),A))) -> p$198 [expansion from 71] 79 + p$197,eta(a,b)=>(eta(app(s,a),app(s,b))=>?A.((A=app(t,a)or eta(app(t,a),A))and(A=app(s,b)or eta(app(s,b),A))))and(eta(app(a,s),app(b,s))=>?B.((B=app(a,t)or eta(app(a,t),B))and(B=app(b,s)or eta(app(b,s),B)))) -> p$199 [expansion from 75] 80 + p$197,eta(s,x)and(eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A)))) [expansion from 75] 81 + (eta(app(s,u),app(x,u))=>?A.((A=app(t,u)or eta(app(t,u),A))and(A=app(x,u)or eta(app(x,u),A))))and(eta(app(u,s),app(u,x))=>?B.((B=app(u,t)or eta(app(u,t),B))and(B=app(u,x)or eta(app(u,x),B)))) -> p$197 [expansion from 75] 82 + eta(app(s,u),app(x,u))=>?A.((A=app(t,u)or eta(app(t,u),A))and(A=app(x,u)or eta(app(x,u),A))),eta(app(u,s),app(u,x))=>?B.((B=app(u,t)or eta(app(u,t),B))and(B=app(u,x)or eta(app(u,x),B))) -> p$197 [expansion from 81] 83 + p$196,~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)),p$198,p$199 -> [expansion from 76] 84 + p$196,~free(s,0)and eta(s,t) [expansion from 76] 85 + eta(abs(app(s,var(0))),subst(s,0,u))and eta(abs(app(s,var(0))),abs(app(t,var(0))))=>?A.((A=subst(s,0,u)or eta(subst(s,0,u),A))and(A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A))) -> p$196 [expansion from 76] 86 + p$195,p$198 [expansion from 77] 87 + p$195 -> eta(s,t)and eta(s,x) [expansion from 77] 88 + p$195 -> eta(s,t)and eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 77] 89 + p$195,eta(s,t),eta(s,x) -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 88] 90 + p$194 -> p$198 [expansion from 78] 92 + ?A.((A=abs(t)or eta(abs(t),A))and(A=abs(x)or eta(abs(x),A))) -> p$194 [expansion from 78] 93 + A=abs(t)or eta(abs(t),A),A=abs(x)or eta(abs(x),A) -> p$194 [expansion from 92] 94 + p$193,p$197 -> p$199 [expansion from 79] 95 + p$193,eta(a,b) [expansion from 79] 96 + (eta(app(s,a),app(s,b))=>?A.((A=app(t,a)or eta(app(t,a),A))and(A=app(s,b)or eta(app(s,b),A))))and(eta(app(a,s),app(b,s))=>?B.((B=app(a,t)or eta(app(a,t),B))and(B=app(b,s)or eta(app(b,s),B)))) -> p$193 [expansion from 79] 97 + ?A.((A=app(t,a)or eta(app(t,a),A))and(A=app(s,b)or eta(app(s,b),A))) and?B.((B=app(a,t)or eta(app(a,t),B))and(B=app(b,s)or eta(app(b,s),B))) -> p$193 [reduction of 96 by [40,95,L,41,95,L]] 98 + A=app(t,a)or eta(app(t,a),A),A=app(s,b)or eta(app(s,b),A),B=app(a,t)or eta(app(a,t),B),B=app(b,s)or eta(app(b,s),B) -> p$193 [expansion from 97] 99 + p$8,A=app(a,t)or eta(app(a,t),A),A=app(b,s)or eta(app(b,s),A) -> p$193 [variable elimination from 98] 100 + A=app(t,a)or eta(app(t,a),A),A=app(s,b)or eta(app(s,b),A) -> p$8 [variable elimination from 98] 101 + p$191,p$197 [expansion from 80] 102 + p$191 -> eta(s,x) [expansion from 80] 103 + p$191 -> eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 80] 104 + p$191,eta(s,x) -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 103] 105 + p$190,eta(app(u,s),app(u,x))=>?A.((A=app(u,t)or eta(app(u,t),A))and(A=app(u,x)or eta(app(u,x),A))) -> p$197 [expansion from 82] 107 + ?A.((A=app(t,u)or eta(app(t,u),A))and(A=app(x,u)or eta(app(x,u),A))) -> p$190 [expansion from 82] 108 + A=app(t,u)or eta(app(t,u),A),A=app(x,u)or eta(app(x,u),A) -> p$190 [expansion from 107] 109 + p$189,p$196 [expansion from 84] 110 + p$189 -> ~free(s,0) [expansion from 84] 111 + p$189 -> eta(s,t) [expansion from 84] 112 + p$189,free(s,0) -> [expansion from 110] 113 + p$188 -> p$196 [expansion from 85] 115 + ?A.((A=subst(s,0,u)or eta(subst(s,0,u),A))and(A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A))) -> p$188 [expansion from 85] 116 + A=subst(s,0,u)or eta(subst(s,0,u),A),A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A) -> p$188 [expansion from 115] 120 + p$186(A),A=abs(t)or eta(abs(t),A) -> p$194 [expansion from 93] 121 + A=abs(x) -> p$186(A) [expansion from 93] 122 + eta(abs(x),A) -> p$186(A) [expansion from 93] 123 + p$185(A),A=app(b,s)or eta(app(b,s),A),p$8 -> p$193 [expansion from 99] 125 + eta(app(a,t),A) -> p$185(A) [expansion from 99] 126 + p$184(A),A=app(s,b)or eta(app(s,b),A) -> p$8 [expansion from 100] 128 + eta(app(t,a),A) -> p$184(A) [expansion from 100] 129 + p$183,p$190 -> p$197 [expansion from 105] 131 + ?A.((A=app(u,t)or eta(app(u,t),A))and(A=app(u,x)or eta(app(u,x),A))) -> p$183 [expansion from 105] 132 + A=app(u,t)or eta(app(u,t),A),A=app(u,x)or eta(app(u,x),A) -> p$183 [expansion from 131] 133 + p$182(A),A=app(t,u)or eta(app(t,u),A) -> p$190 [expansion from 108] 134 + A=app(x,u) -> p$182(A) [expansion from 108] 135 + eta(app(x,u),A) -> p$182(A) [expansion from 108] 139 + p$180(A),A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A) -> p$188 [expansion from 116] 141 + eta(subst(s,0,u),A) -> p$180(A) [expansion from 116] 142 + p$179(A),p$186(A) -> p$194 [expansion from 120] 143 + A=abs(t) -> p$179(A) [expansion from 120] 144 + eta(abs(t),A) -> p$179(A) [expansion from 120] 145 + p$186(abs(x)) [reflexivity resolution from 121] 146 + p$178(A),p$185(A),p$8 -> p$193 [expansion from 123] 148 + eta(app(b,s),A) -> p$178(A) [expansion from 123] 150 + p$177(A),p$184(A) -> p$8 [expansion from 126] 152 + eta(app(s,b),A) -> p$177(A) [expansion from 126] 154 + p$176(A),A=app(u,t)or eta(app(u,t),A) -> p$183 [expansion from 132] 155 + A=app(u,x) -> p$176(A) [expansion from 132] 156 + eta(app(u,x),A) -> p$176(A) [expansion from 132] 157 + p$175(A),p$182(A) -> p$190 [expansion from 133] 158 + A=app(t,u) -> p$175(A) [expansion from 133] 159 + eta(app(t,u),A) -> p$175(A) [expansion from 133] 160 + p$182(app(x,u)) [reflexivity resolution from 134] 161 + p$174(A),p$180(A) -> p$188 [expansion from 139] 163 + eta(abs(app(t,var(0))),A) -> p$174(A) [expansion from 139] 165 + p$179(abs(t)) [reflexivity resolution from 143] 168 + p$173(A),p$176(A) -> p$183 [expansion from 154] 169 + A=app(u,t) -> p$173(A) [expansion from 154] 170 + eta(app(u,t),A) -> p$173(A) [expansion from 154] 171 + p$176(app(u,x)) [reflexivity resolution from 155] 172 + p$175(app(t,u)) [reflexivity resolution from 158] 174 + p$173(app(u,t)) [reflexivity resolution from 169] 175 + p$197,eta(s,x) [negative chaining of 101 from 102] 176 + p$196,eta(s,t) [negative chaining of 109 from 111] 186 + p$186(abs(t)) -> p$194 [negative chaining of 165 from 142] 188 + p$182(app(t,u)) -> p$190 [negative chaining of 172 from 157] 189 + p$176(app(u,t)) -> p$183 [negative chaining of 174 from 168] 190 + p$198,eta(s,t)and eta(s,x) [negative chaining of 86 from 87] 191 + p$172,p$198 [expansion from 190] 192 + p$172 -> eta(s,t) [expansion from 190] 193 + p$172 -> eta(s,x) [expansion from 190] 194 + p$198,eta(s,t) [negative chaining of 191 from 192] 195 + p$198,eta(s,x) [negative chaining of 191 from 193] 198 + eta(x,A) -> p$186(abs(A)) [negative chaining of 42 from 122] 199 + eta(t,A) -> p$179(abs(A)) [negative chaining of 42 from 144] 200 + eta(a,A) -> p$185(app(A,t)) [negative chaining of 40 from 125] 202 + eta(x,A) -> p$182(app(A,u)) [negative chaining of 40 from 135] 204 + eta(s,A) -> p$177(app(A,b)) [negative chaining of 40 from 152] 206 + eta(t,A) -> p$175(app(A,u)) [negative chaining of 40 from 159] 208 + p$193,p$185(app(b,t)) [negative chaining of 95 from 200] 209 + p$199,p$177(app(t,b)) [negative chaining of 72 from 204] 214 + p$184(app(t,b)) -> p$199,p$8 [negative chaining of 209 from 150] 220 + eta(a,A) -> p$184(app(t,A)) [negative chaining of 41 from 128] 222 + eta(s,A) -> p$178(app(b,A)) [negative chaining of 41 from 148] 224 + eta(x,A) -> p$176(app(u,A)) [negative chaining of 41 from 156] 226 + eta(t,A) -> p$173(app(u,A)) [negative chaining of 41 from 170] 227 + p$193,p$184(app(t,b)) [negative chaining of 95 from 220] 228 + p$199,p$178(app(b,t)) [negative chaining of 72 from 222] 233 + p$193,p$199,p$8 [negative chaining of 227 from 214] 236 + p$8,p$185(app(b,t)) -> p$199,p$193 [negative chaining of 228 from 146] 237 + p$193,p$199 [reduction of 236 by [233,208]] 289 + p$191 -> p$197,?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [negative chaining of 175 from 104] 291 + ?A.((A=t or eta(t,A))and(A=x or eta(x,A))),p$197 [reduction of 289 by [101]] 292 + p$171,p$197 [expansion from 291] 293 + p$171 -> (s$3=t or eta(t,s$3))and(s$3=x or eta(x,s$3)) [expansion from 291] 294 + p$197,(s$3=t or eta(t,s$3))and(s$3=x or eta(x,s$3)) [negative chaining of 292 from 293] 295 + p$170,p$197 [expansion from 294] 296 + p$170 -> s$3=t or eta(t,s$3) [expansion from 294] 297 + p$170 -> s$3=x or eta(x,s$3) [expansion from 294] 298 + p$170 -> s$3=t,eta(t,s$3) [expansion from 296] 299 + p$170 -> s$3=x,eta(x,s$3) [expansion from 297] 300 + p$197,eta(t,s$3),s$3=t [negative chaining of 295 from 298] 301 + p$197,eta(x,s$3),s$3=x [negative chaining of 295 from 299] 304 + p$197,s$3=t,p$175(app(s$3,u)) [negative chaining of 300 from 206] 306 + p$197,s$3=t,p$173(app(u,s$3)) [negative chaining of 300 from 226] 310 + p$197,s$3=x,p$182(app(s$3,u)) [negative chaining of 301 from 202] 311 + p$197,s$3=x,p$176(app(u,s$3)) [negative chaining of 301 from 224] 394 + p$182(app(s$3,u)) -> p$197,s$3=t,p$190 [negative chaining of 304 from 157] 407 + p$176(app(u,s$3)) -> p$197,s$3=t,p$183 [negative chaining of 306 from 168] 418 + p$197,s$3=x,p$197,s$3=t,p$190 [negative chaining of 310 from 394] 421 + s$3=x,p$197,s$3=t,p$190 [condensement of 418] 427 + eta(t,x),p$197,s$3=t,p$190,p$197,s$3=t [chaining of 421 from 300] 440 + eta(t,x),p$190,p$197,s$3=t [condensement of 427] 441 + s$3=t,p$197,p$190 [reduction of 440 by [206,157,160,L,L]] 455 + eta(x,t),p$197,p$190,p$197,s$3=x [chaining of 441 from 301] 469 + eta(x,t),p$190,p$197,s$3=x [condensement of 455] 470 + p$190,p$197,t=x [reduction of 469 by [202,188,L,L,441]] 484 + p$182(app(t,u)),p$197,p$190 [chaining of 470 from 160] 515 + p$190,p$197 [reduction of 484 by [188,L]] 528 + p$197,s$3=x,p$197,s$3=t,p$183 [negative chaining of 311 from 407] 533 + s$3=x,p$197,s$3=t,p$183 [condensement of 528] 534 + s$3=x,p$197,s$3=t [reduction of 533 by [129,515,L]] 544 + eta(t,x),p$197,s$3=t,p$197,s$3=t [chaining of 534 from 300] 559 + eta(t,x),p$197,s$3=t [condensement of 544] 560 + s$3=t,p$197 [reduction of 559 by [226,168,129,515,L,171,L,L]] 576 + eta(x,t),p$197,p$197,s$3=x [chaining of 560 from 301] 592 + eta(x,t),p$197,s$3=x [condensement of 576] 593 + p$197,t=x [reduction of 592 by [224,189,129,515,L,L,L,560]] 610 + p$176(app(u,t)),p$197 [chaining of 593 from 171] 641 + p$197 [reduction of 610 by [189,129,515,L,L]] 651 + p$199 [reduction of 94 by [237,641]] 652 + ~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)),p$196,p$198 -> [reduction of 83 by [651]] 657 + p$196,free(t,A)==free(s,A),A<0 [negative chaining of 176 from 66] 841 + eta(s,t),p$195 -> p$198,?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [negative chaining of 195 from 89] 842 + ?A.((A=t or eta(t,A))and(A=x or eta(x,A))),p$198 [reduction of 841 by [194,86]] 843 + p$171,p$198 [expansion from 842] 844 + p$198,(s$3=t or eta(t,s$3))and(s$3=x or eta(x,s$3)) [negative chaining of 843 from 293] 845 + p$170,p$198 [expansion from 844] 846 + p$198,eta(t,s$3),s$3=t [negative chaining of 845 from 298] 847 + p$198,eta(x,s$3),s$3=x [negative chaining of 845 from 299] 848 + p$198,s$3=t,p$179(abs(s$3)) [negative chaining of 846 from 199] 860 + p$198,s$3=x,p$186(abs(s$3)) [negative chaining of 847 from 198] 869 + p$186(abs(s$3)) -> p$198,s$3=t,p$194 [negative chaining of 848 from 142] 870 + p$186(abs(s$3)) -> p$198,s$3=t [reduction of 869 by [90,L]] 871 + p$198,s$3=x,p$198,s$3=t [negative chaining of 860 from 870] 872 + s$3=x,p$198,s$3=t [condensement of 871] 876 + eta(t,x),p$198,s$3=t,p$198,s$3=t [chaining of 872 from 846] 881 + eta(t,x),p$198,s$3=t [condensement of 876] 882 + s$3=t,p$198 [reduction of 881 by [199,142,90,L,145,L,L]] 888 + eta(x,t),p$198,p$198,s$3=x [chaining of 882 from 847] 894 + eta(x,t),p$198,s$3=x [condensement of 888] 895 + p$198,t=x [reduction of 894 by [198,186,90,L,L,L,882]] 900 + p$186(abs(t)),p$198 [chaining of 895 from 145] 938 + p$198 [reduction of 900 by [186,90,L,L]] 948 + ~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)),p$196 -> [reduction of 652 by [938]] 1050 + eta(s,A) -> p$180(subst(A,0,u)) [negative chaining of 69 from 141] 1065 + p$196,p$180(subst(t,0,u)) [negative chaining of 176 from 1050] 1145 + free(t,0),p$174(subst(t,0,A)) [negative chaining of 62 from 163] 1169 + free(s,0),p$196,p$174(subst(t,0,A)) {[conj([free(t,0)>A],[],[])]} [chaining of 657 from 1145] 1171 + p$174(subst(t,0,A)),p$196 {[conj([free(t,0)>A],[],[])]} [reduction of 1169 by [112,109,L]] 1172 + p$180(subst(t,0,A)) -> p$196,p$188 {[conj([free(t,0)>A],[],[])]} [negative chaining of 1171 from 161] 1173 + p$180(subst(t,0,A)) -> p$196 {[conj([free(t,0)>A],[],[])]} [reduction of 1172 by [113,L]] 1174 + p$196,p$196 [negative chaining of 1065 from 1173] 1175 + p$196 [condensement of 1174] 1176 + ~free(s,0)=>eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> [reduction of 948 by [1175]] 1177 + ~free(s,0) [expansion from 1176] 1178 + eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> [expansion from 1176] 1179 + free(s,0) -> [expansion from 1177] 1180 + ?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> [reduction of 1178 by [62,1179,L,L]] 1181 + A=subst(s,0,u)or eta(subst(s,0,u),A) -> [expansion from 1180] 1182 + A=subst(s,0,u) -> [expansion from 1181] Length = 209, Depth = 45 Total time: 513340 milliseconds Number of forward inferences: 721 Number of tableau inferences: 119 Number of kept clauses: 558 */