use(subst). 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))) -> []. precedence([0,a,x,u,t]). top_predicates_precedence([lemmaE8,lemmaE1,lemmaE2]). option([var_overlaps(off),search_depth(0)]). :-sarp(+[15]),saci([2]). /* 20020823 since we now select abbreviations when possible sama([2]) is not appropriate */ /* certainly not a sama([2]) proof! Proof: ====== 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 : 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] 32 : lemmaE2(A,B,C,D)==(0=eta(subst(A,D,C),subst(B,D,C))) [input] 33 : lemmaE1(A,B,C)==(0=free(B,C)<=>free(A,C)) [input] 34 : lemmaE1(A,B,C) [input] 35 : lemmaE2(A,B,C,D) [input] 36 + ~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] 37 : 0=free(C,A)<=>free(B,A) [reduction of 34 by [33]] 38 : 0= free(C,A)==free(B,A) [expansion from 37] 39 : eta(A,B) -> C<0,free(B,C)==free(A,C) [totality resolution from 38] v 40 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 35 by [32]] 41 : 0= eta(subst(B,A,D),subst(C,A,D)) [expansion from 40] 42 : eta(A,B) -> C<0,eta(subst(A,C,D),subst(B,C,D)) [totality resolution from 41] 43 + 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 36 by [31,L,L,31,31,31,31,31,31,31,31]] 44 + q$499,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 43] 45 + q$499,eta(s,t) [expansion from 43] 46 + (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))))) -> q$499 [expansion from 43] 50 + (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))))) -> q$499 [reduction of 46 by [29,45,L,28,45,L,29,45,L,28,45,L,45,L]] 51 + 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)))) -> q$499 [expansion from 50] 55 + q$498,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)))) -> q$499 [expansion from 51] 56 + q$498,eta(s,x)and(eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A)))) [expansion from 51] 57 + (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)))) -> q$498 [expansion from 51] 59 + 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))) -> q$498 [expansion from 57] 60 + q$497,q$498 -> q$499 [expansion from 55] 61 + q$497,eta(a,b) [expansion from 55] 62 + (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)))) -> q$497 [expansion from 55] 63 + q$496,q$498 [expansion from 56] 64 + q$496 -> eta(s,x) [expansion from 56] 65 + q$496 -> eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 56] 66 + ?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))) -> q$497 [reduction of 62 by [28,61,L,29,61,L]] 67 + 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) -> q$497 [expansion from 66] 68 + q$496 -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [reduction of 65 by [64,L]] 69 + q$495,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))) -> q$498 [expansion from 59] 71 + ?A.((A=app(t,u)or eta(app(t,u),A))and(A=app(x,u)or eta(app(x,u),A))) -> q$495 [expansion from 59] 72 + q$494(A),B=app(s,b)or eta(app(s,b),B),A=app(b,s)or eta(app(b,s),A),B=app(t,a)or eta(app(t,a),B) -> q$497 [expansion from 67] 74 + eta(app(a,t),A) -> q$494(A) [expansion from 67] 75 + q$495,?A.((A=app(u,t)or eta(app(u,t),A))and(A=app(u,x)or eta(app(u,x),A))) -> q$498 [reduction of 69 by [29,64,63,L]] 76 + q$495,A=app(u,t)or eta(app(u,t),A),A=app(u,x)or eta(app(u,x),A) -> q$498 [expansion from 75] 77 + A=app(t,u)or eta(app(t,u),A),A=app(x,u)or eta(app(x,u),A) -> q$495 [expansion from 71] 78 + q$496 -> q$493 [expansion from 68] 79 + q$493 -> (s$3=t or eta(t,s$3))and(s$3=x or eta(x,s$3)) [expansion from 68] 81 + q$492(A),A=app(t,u)or eta(app(t,u),A) -> q$495 [expansion from 77] 82 + A=app(x,u) -> q$492(A) [expansion from 77] 83 + eta(app(x,u),A) -> q$492(A) [expansion from 77] 85 + q$493 -> q$491 [expansion from 79] 86 + q$491 -> s$3=t or eta(t,s$3) [expansion from 79] 87 + q$491 -> s$3=x or eta(x,s$3) [expansion from 79] 88 + q$491 -> s$3=t,eta(t,s$3) [expansion from 86] 89 + q$491 -> s$3=x,eta(x,s$3) [expansion from 87] 90 + q$490(A),q$492(A) -> q$495 [expansion from 81] 91 + A=app(t,u) -> q$490(A) [expansion from 81] 92 + eta(app(t,u),A) -> q$490(A) [expansion from 81] 93 + q$492(app(x,u)) [reflexivity resolution from 82] 94 + q$490(app(t,u)) [reflexivity resolution from 91] 97 + eta(a,A) -> q$494(app(A,t)) [negative chaining of 28 from 74] 99 + q$492(app(t,u)) -> q$495 [negative chaining of 94 from 90] 100 + eta(x,A) -> q$492(app(A,u)) [negative chaining of 28 from 83] 102 + eta(t,A) -> q$490(app(A,u)) [negative chaining of 28 from 92] 104 + q$497,q$494(app(b,t)) [negative chaining of 61 from 97] 107 + q$491 -> s$3=t,q$490(app(s$3,u)) [negative chaining of 88 from 102] 109 + q$491 -> s$3=x,q$492(app(s$3,u)) [negative chaining of 89 from 100] 111 + q$491,q$492(app(s$3,u)) -> s$3=t,q$495 [negative chaining of 107 from 90] 122 + q$491,q$491 -> s$3=x,q$495,s$3=t [negative chaining of 109 from 111] 123 + q$491 -> s$3=x,q$495,s$3=t [condensement of 122] 126 + q$491,q$491 -> eta(t,x),q$495,s$3=t,s$3=t [chaining of 123 from 88] 133 + q$491 -> eta(t,x),q$495,s$3=t [condensement of 126] 134 + q$491 -> s$3=t,q$495 [reduction of 133 by [102,90,93,L,L]] 141 + q$491,q$491 -> eta(x,t),q$495,s$3=x [chaining of 134 from 89] 148 + q$491 -> eta(x,t),q$495,s$3=x [condensement of 141] 149 + q$491 -> q$495,t=x [reduction of 148 by [100,99,L,L,134]] 155 + q$491 -> q$492(app(t,u)),q$495 [chaining of 149 from 93] 163 + q$491 -> q$495 [reduction of 155 by [99,L]] 166 + q$493 -> q$495 [negative chaining of 85 from 163] 170 + q$496 -> q$495 [negative chaining of 78 from 166] 179 + q$496,A=app(u,t)or eta(app(u,t),A),A=app(u,x)or eta(app(u,x),A) -> q$498 [negative chaining of 170 from 76] 181 + A=app(s,b)or eta(app(s,b),A),A=app(t,a)or eta(app(t,a),A),app(b,t)=app(b,s)or eta(app(b,s),app(b,t)) -> q$497,q$497 [negative chaining of 104 from 72] 183 + A=app(u,x)or eta(app(u,x),A),A=app(u,t)or eta(app(u,t),A) -> q$498 [reduction of 179 by [63]] 184 + A=app(s,b)or eta(app(s,b),A),A=app(t,a)or eta(app(t,a),A),app(b,t)=app(b,s)or eta(app(b,s),app(b,t)) -> q$497 [condensement of 181] 185 + q$487(A),A=app(u,t)or eta(app(u,t),A) -> q$498 [expansion from 183] 186 + A=app(u,x) -> q$487(A) [expansion from 183] 187 + eta(app(u,x),A) -> q$487(A) [expansion from 183] 191 + q$485,A=app(s,b)or eta(app(s,b),A),A=app(t,a)or eta(app(t,a),A) -> q$497 [expansion from 184] 193 + eta(app(b,s),app(b,t)) -> q$485 [expansion from 184] 194 + q$484(A),q$487(A) -> q$498 [expansion from 185] 195 + A=app(u,t) -> q$484(A) [expansion from 185] 196 + eta(app(u,t),A) -> q$484(A) [expansion from 185] 197 + q$487(app(u,x)) [reflexivity resolution from 186] 198 + q$484(app(u,t)) [reflexivity resolution from 195] 200 + eta(s,t) -> q$485 [negative chaining of 29 from 193] 202 + q$499,q$485 [negative chaining of 45 from 200] 203 + q$487(app(u,t)) -> q$498 [negative chaining of 198 from 194] 205 + eta(x,A) -> q$487(app(u,A)) [negative chaining of 29 from 187] 208 + eta(t,A) -> q$484(app(u,A)) [negative chaining of 29 from 196] 209 + q$491 -> s$3=x,q$487(app(u,s$3)) [negative chaining of 89 from 205] 211 + q$491 -> s$3=t,q$484(app(u,s$3)) [negative chaining of 88 from 208] 219 + q$491,q$487(app(u,s$3)) -> s$3=t,q$498 [negative chaining of 211 from 194] 223 + q$487(app(u,s$3)) -> q$498,s$3=t [reduction of 219 by [85,78,63]] 227 + q$491 -> s$3=x,q$498,s$3=t [negative chaining of 209 from 223] 230 + s$3=t,q$498,s$3=x [reduction of 227 by [85,78,63]] 234 + q$491 -> eta(t,x),q$498,s$3=t,s$3=t [chaining of 230 from 88] 246 + q$491 -> eta(t,x),q$498,s$3=t [condensement of 234] 247 + s$3=t,q$498 [reduction of 246 by [85,78,63,208,194,197,L,L]] 255 + q$491 -> eta(x,t),q$498,s$3=x [chaining of 247 from 89] 265 + q$498,t=x [reduction of 255 by [85,78,63,205,203,L,L,247]] 278 + q$498,q$487(app(u,t)) [negative chaining of 265 from 186] 284 + q$498 [reduction of 278 by [203,L]] 285 + q$497 -> q$499 [reduction of 60 by [284]] 286 + A=app(s,b)or eta(app(s,b),A),A=app(t,a)or eta(app(t,a),A) -> q$499,q$497 [negative chaining of 202 from 191] 296 + A=app(s,b)or eta(app(s,b),A),A=app(t,a)or eta(app(t,a),A) -> q$499 [reduction of 286 by [285,L]] 301 + q$483(A),A=app(s,b)or eta(app(s,b),A) -> q$499 [expansion from 296] 303 + eta(app(t,a),A) -> q$483(A) [expansion from 296] 305 + q$482(A),q$483(A) -> q$499 [expansion from 301] 307 + eta(app(s,b),A) -> q$482(A) [expansion from 301] 311 + eta(a,A) -> q$483(app(t,A)) [negative chaining of 29 from 303] 312 + eta(s,A) -> q$482(app(A,b)) [negative chaining of 28 from 307] 316 + q$497,q$483(app(t,b)) [negative chaining of 61 from 311] 317 + q$499,q$482(app(t,b)) [negative chaining of 45 from 312] 319 + q$499 [reduction of 317 by [305,316,285,L,L]] 320 + ~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)),~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))))=>?B.((B=subst(s,0,u)or eta(subst(s,0,u),B))and(B=abs(app(t,var(0)))or eta(abs(app(t,var(0))),B))),eta(s,t)and eta(s,x)and(eta(s,t)and eta(s,x)=>?C.((C=t or eta(t,C))and(C=x or eta(x,C))))=>eta(abs(s),abs(t))and eta(abs(s),abs(x))=>?D.((D=abs(t)or eta(abs(t),D))and(D=abs(x)or eta(abs(x),D))) -> [reduction of 44 by [319]] 321 + q$481,~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)) -> [expansion from 320] 322 + q$481,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 320] 323 + 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))) -> q$481 [expansion from 320] 325 + q$480,q$481,~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))) -> [expansion from 321] 326 + q$480,~free(s,0) [expansion from 321] 327 + eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> q$480 [expansion from 321] 328 + q$479,q$481 [expansion from 322] 329 + q$479 -> eta(s,t)and eta(s,x) [expansion from 322] 330 + q$479 -> eta(s,t)and eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 322] 331 + free(s,0) -> q$480 [expansion from 326] 332 + ?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> q$480 [reduction of 327 by [30,331,L,L]] 333 + A=subst(s,0,u)or eta(subst(s,0,u),A) -> q$480 [expansion from 332] 334 + q$479 -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [reduction of 330 by [329,L]] 335 + q$478 -> q$481 [expansion from 323] 337 + ?A.((A=abs(t)or eta(abs(t),A))and(A=abs(x)or eta(abs(x),A))) -> q$478 [expansion from 323] 338 + q$477(A) -> q$480 [expansion from 333] 339 + A=subst(s,0,u) -> q$477(A) [expansion from 333] 340 + eta(subst(s,0,u),A) -> q$477(A) [expansion from 333] 341 + A=abs(t)or eta(abs(t),A),A=abs(x)or eta(abs(x),A) -> q$478 [expansion from 337] 345 + q$479 -> q$493 [expansion from 334] 349 + q$474(A),A=abs(t)or eta(abs(t),A) -> q$478 [expansion from 341] 350 + A=abs(x) -> q$474(A) [expansion from 341] 351 + eta(abs(x),A) -> q$474(A) [expansion from 341] 352 + q$477(subst(s,0,u)) [reflexivity resolution from 339] 353 + q$473(A),q$474(A) -> q$478 [expansion from 349] 354 + A=abs(t) -> q$473(A) [expansion from 349] 355 + eta(abs(t),A) -> q$473(A) [expansion from 349] 356 + q$474(abs(x)) [reflexivity resolution from 350] 357 + q$473(abs(t)) [reflexivity resolution from 354] 358 + q$481,q$493 [negative chaining of 328 from 345] 363 + q$472,q$481,q$480 -> [expansion from 325] 364 + q$472,~free(s,0)and eta(s,t) [expansion from 325] 365 + 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))) -> q$472 [expansion from 325] 367 + q$471,q$472 [expansion from 364] 368 + q$471 -> ~free(s,0) [expansion from 364] 369 + q$471 -> eta(s,t) [expansion from 364] 370 + q$470 -> q$472 [expansion from 365] 372 + ?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))) -> q$470 [expansion from 365] 373 + q$471,free(s,0) -> [expansion from 368] 374 + 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) -> q$470 [expansion from 372] 378 + q$477(A),A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A) -> q$470 [expansion from 374] 379 + q$468(A),q$477(A) -> q$470 [expansion from 378] 381 + eta(abs(app(t,var(0))),A) -> q$468(A) [expansion from 378] 382 + q$480 [negative chaining of 352 from 338] 383 + q$472,q$481 -> [reduction of 363 by [382]] 385 + q$471 -> free(t,A)==free(s,A),A<0 [negative chaining of 369 from 39] 402 + q$474(abs(t)) -> q$478 [negative chaining of 357 from 353] 403 + eta(x,A) -> q$474(abs(A)) [negative chaining of 27 from 351] 406 + eta(t,A) -> q$473(abs(A)) [negative chaining of 27 from 355] 408 + q$491 -> s$3=x,q$474(abs(s$3)) [negative chaining of 89 from 403] 411 + q$491 -> s$3=t,q$473(abs(s$3)) [negative chaining of 88 from 406] 412 + q$472,free(t,A)==free(s,A),A<0 [negative chaining of 367 from 385] 460 + q$491,q$474(abs(s$3)) -> s$3=t,q$478 [negative chaining of 411 from 353] 608 + eta(s,A) -> q$477(subst(A,0,u)) [negative chaining of 42 from 340] 611 + q$471 -> q$477(subst(t,0,u)) [negative chaining of 369 from 608] 833 + free(t,0),q$468(subst(t,0,A)) [negative chaining of 30 from 381] 851 + free(s,0),q$472,q$468(subst(t,0,A)) {[conj([free(t,0)>A],[],[])]} [chaining of 412 from 833] 854 + q$468(subst(t,0,A)),q$472 {[conj([free(t,0)>A],[],[])]} [reduction of 851 by [373,367,L]] 855 + q$477(subst(t,0,A)) -> q$472,q$470 {[conj([free(t,0)>A],[],[])]} [negative chaining of 854 from 379] 862 + q$477(subst(t,0,A)) -> q$472 {[conj([free(t,0)>A],[],[])]} [reduction of 855 by [370,L]] 890 + q$471 -> q$472 [negative chaining of 611 from 862] 937 + q$472 [reduction of 890 by [367]] 938 + q$481 -> [reduction of 383 by [937]] 939 + q$478 -> [reduction of 335 by [938,L]] 941 + q$493 [reduction of 358 by [938,L]] 942 + q$491 [reduction of 85 by [941]] 949 + q$473(A),q$474(A) -> [reduction of 353 by [939,L]] 950 + q$474(abs(t)) -> [reduction of 402 by [939,L]] 951 + q$474(abs(s$3)) -> s$3=t [reduction of 460 by [942,939,L]] 977 + s$3=x,eta(x,s$3) [reduction of 89 by [942]] 994 + s$3=x,q$474(abs(s$3)) [reduction of 408 by [942]] 995 + s$3=t,q$473(abs(s$3)) [reduction of 411 by [942]] 1151 + s$3=x,s$3=t [negative chaining of 994 from 951] 1152 + q$474(abs(s$3)) -> s$3=t [negative chaining of 995 from 949] 1168 + s$3=t [reduction of 1152 by [1151,356]] 1173 + t=x [reduction of 977 by [1168,403,950,L,L,1168]] 1189 + A=abs(t) -> q$474(A) [reduction of 350 by [1173]] 1203 + q$474(abs(t)) [reflexivity resolution from 1189] 1207 + false [reduction of 1203 by [950,L]] Length = 201, Depth = 75 Total time: 143410 milliseconds Number of forward inferences: 691 Number of tableau inferences: 163 Number of kept clauses: 641 */ /* 20020823 newer abbreviations greater in the ordering than older ones option([var_overlaps(off),search_depth(0)]). :-sarp(+[15]),saci([2]),sama([]). Proof: ====== 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 : 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] 32 : lemmaE2(A,B,C,D)==(0=eta(subst(A,D,C),subst(B,D,C))) [input] 33 : lemmaE1(A,B,C)==(0=free(B,C)<=>free(A,C)) [input] 34 : lemmaE1(A,B,C) [input] 35 : lemmaE2(A,B,C,D) [input] 36 + ~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] 37 : 0=free(C,A)<=>free(B,A) [reduction of 34 by [33]] 38 : 0= free(C,A)==free(B,A) [condensement of 37] 39 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 35 by [32]] 40 : 0= eta(subst(B,A,D),subst(C,A,D)) [condensement of 39] 41 + 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 36 by [31,L,L,31,31,31,31,31,31,31,31]] 42 + q$499,~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)),eta(s,t)and eta(s,x)and(eta(s,t)and eta(s,x)=>?B.((B=t or eta(t,B))and(B=x or eta(x,B))))=>eta(abs(s),abs(t))and eta(abs(s),abs(x))=>?C.((C=abs(t)or eta(abs(t),C))and(C=abs(x)or eta(abs(x),C))),~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))))=>?D.((D=subst(s,0,u)or eta(subst(s,0,u),D))and(D=abs(app(t,var(0)))or eta(abs(app(t,var(0))),D))) -> [expansion from 41] 43 + q$499,eta(s,t) [expansion from 41] 44 + 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)))),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)))) -> q$499 [expansion from 41] 45 + 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)))) -> q$499 [reduction of 44 by [29,43,L,28,43,L,43,L,29,43,L,28,43,L]] 46 + q$498,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))),q$499,~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))) -> [expansion from 42] 47 + q$498,~free(s,0) [expansion from 42] 48 + eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> q$498 [expansion from 42] 49 + q$497,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)))) -> q$499 [expansion from 45] 50 + q$497,eta(s,x)and(eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A)))) [expansion from 45] 51 + 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))) -> q$497 [expansion from 45] 53 + free(s,0) -> q$498 [reduction of 47 by [L]] 54 + ?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> q$498 [reduction of 48 by [30,53,L,L]] 55 + A=subst(s,0,u)or eta(subst(s,0,u),A) -> q$498 [condensement of 54] 57 + q$496,~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))),q$498,q$499 -> [expansion from 46] 58 + q$496,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 46] 59 + 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))) -> q$496 [expansion from 46] 60 + A=subst(s,0,u) -> q$498 [expansion from 55] 62 + q$495,q$497 -> q$499 [expansion from 49] 63 + q$495,eta(a,b) [expansion from 49] 64 + 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))),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))) -> q$495 [expansion from 49] 65 + q$494,q$497 [expansion from 50] 66 + q$494 -> eta(s,x) [expansion from 50] 67 + eta(s,x),q$494 -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 50] 68 + q$493,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))) -> q$497 [expansion from 51] 70 + A=app(u,t)or eta(app(u,t),A),A=app(u,x)or eta(app(u,x),A) -> q$493 [expansion from 51] 71 + ?A.((A=app(t,a)or eta(app(t,a),A))and(A=app(s,b)or eta(app(s,b),A))),?B.((B=app(a,t)or eta(app(a,t),B))and(B=app(b,s)or eta(app(b,s),B))) -> q$495 [reduction of 64 by [29,63,L,28,63,L]] 72 + 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) -> q$495 [condensement of 71] 73 + q$494 -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [reduction of 67 by [66]] 74 + q$492,q$496,q$498,q$499 -> [expansion from 57] 75 + q$492,~free(s,0)and eta(s,t) [expansion from 57] 76 + 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))) -> q$492 [expansion from 57] 77 + q$491,q$496 [expansion from 58] 78 + q$491 -> eta(s,t)and eta(s,x) [expansion from 58] 79 + eta(s,t),eta(s,x),q$491 -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [expansion from 58] 80 + q$490 -> q$496 [expansion from 59] 82 + A=abs(t)or eta(abs(t),A),A=abs(x)or eta(abs(x),A) -> q$490 [expansion from 59] 83 + q$489(A),B=app(b,s)or eta(app(b,s),B),A=app(t,a)or eta(app(t,a),A),B=app(a,t)or eta(app(a,t),B) -> q$495 [expansion from 72] 85 + eta(app(s,b),A) -> q$489(A) [expansion from 72] 86 + q$494 -> q$488 [expansion from 73] 87 + q$488 -> (s$4=t or eta(t,s$4))and(s$4=x or eta(x,s$4)) [expansion from 73] 89 + q$487,q$493 -> q$497 [expansion from 68] 91 + A=app(t,u)or eta(app(t,u),A),A=app(x,u)or eta(app(x,u),A) -> q$487 [expansion from 68] 92 + q$486(A),A=app(u,t)or eta(app(u,t),A) -> q$493 [expansion from 70] 93 + A=app(u,x) -> q$486(A) [expansion from 70] 94 + eta(app(u,x),A) -> q$486(A) [expansion from 70] 96 + q$485,q$492 [expansion from 75] 97 + q$485 -> ~free(s,0) [expansion from 75] 98 + q$485 -> eta(s,t) [expansion from 75] 99 + q$484 -> q$492 [expansion from 76] 101 + 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) -> q$484 [expansion from 76] 102 + q$491 -> eta(s,t) [expansion from 78] 103 + q$491 -> eta(s,x) [expansion from 78] 104 + q$491,eta(s,t),eta(s,x) -> q$488 [expansion from 79] 107 + q$483(A),A=abs(t)or eta(abs(t),A) -> q$490 [expansion from 82] 108 + A=abs(x) -> q$483(A) [expansion from 82] 109 + eta(abs(x),A) -> q$483(A) [expansion from 82] 110 + q$482(A),B=app(t,a)or eta(app(t,a),B),A=app(a,t)or eta(app(a,t),A),q$489(B) -> q$495 [expansion from 83] 112 + eta(app(b,s),A) -> q$482(A) [expansion from 83] 113 + q$488 -> q$481 [expansion from 87] 114 + q$481 -> s$4=t,eta(t,s$4) [expansion from 87] 115 + q$481 -> s$4=x,eta(x,s$4) [expansion from 87] 116 + q$480(A),A=app(t,u)or eta(app(t,u),A) -> q$487 [expansion from 91] 117 + A=app(x,u) -> q$480(A) [expansion from 91] 118 + eta(app(x,u),A) -> q$480(A) [expansion from 91] 119 + q$479(A),q$486(A) -> q$493 [expansion from 92] 120 + A=app(u,t) -> q$479(A) [expansion from 92] 121 + eta(app(u,t),A) -> q$479(A) [expansion from 92] 122 + q$495,q$497,q$492,q$496,q$498 -> [negative chaining of 62 from 74] 139 + q$485,free(s,0) -> [reduction of 97 by [L]] 140 + q$491 -> q$488 [reduction of 104 by [102,103]] 167 + q$478(A),A=abs(app(t,var(0)))or eta(abs(app(t,var(0))),A) -> q$484 [expansion from 101] 169 + eta(subst(s,0,u),A) -> q$478(A) [expansion from 101] 170 + q$477(A),q$483(A) -> q$490 [expansion from 107] 171 + A=abs(t) -> q$477(A) [expansion from 107] 172 + eta(abs(t),A) -> q$477(A) [expansion from 107] 173 + q$476(A),B=app(a,t)or eta(app(a,t),B),q$489(A),q$482(B) -> q$495 [expansion from 110] 175 + eta(app(t,a),A) -> q$476(A) [expansion from 110] 176 + q$475(A),q$480(A) -> q$487 [expansion from 116] 177 + A=app(t,u) -> q$475(A) [expansion from 116] 178 + eta(app(t,u),A) -> q$475(A) [expansion from 116] 187 + q$485,0= free(t,A)==free(s,A) {[conj([eta(s,t)>A],[],[])]} [negative chaining of 98 from 38] 190 + q$492,q$495,q$496,q$497 -> [negative chaining of 60 from 122] 191 + eta(x,A) -> q$483(abs(A)) [negative chaining of 27 from 109] 194 + A=app(u,x),q$479(A) -> q$493 {[conj([A>=app(u,x)],[],[])]} [negative chaining of 93 from 119] 199 + eta(s,A) -> q$489(app(A,b)) [negative chaining of 28 from 85] 203 + eta(x,A) -> q$480(app(A,u)) [negative chaining of 28 from 118] 207 + q$485 -> A<0,free(t,A)==free(s,A) {[conj([eta(s,t)>A],[],[])]} [totality resolution from 187] 223 + q$474(A),q$478(A) -> q$484 [expansion from 167] 225 + eta(abs(app(t,var(0))),A) -> q$474(A) [expansion from 167] 226 + q$473(A),q$489(B),q$482(A),q$476(B) -> q$495 [expansion from 173] 228 + eta(app(a,t),A) -> q$473(A) [expansion from 173] 253 + q$492,q$495,q$496 -> q$494 [negative chaining of 65 from 190] 254 + q$487,q$493,q$492,q$495,q$496 -> [negative chaining of 89 from 190] 255 + eta(t,A) -> q$477(abs(A)) [negative chaining of 27 from 172] 257 + eta(t,A) -> q$475(app(A,u)) [negative chaining of 28 from 178] 258 + eta(a,A) -> q$473(app(A,t)) [negative chaining of 28 from 228] 259 + q$481 -> s$4=x,q$483(abs(s$4)) [negative chaining of 115 from 191] 261 + q$499,q$489(app(t,b)) [negative chaining of 43 from 199] 262 + q$485 -> q$489(app(t,b)) [negative chaining of 98 from 199] 263 + q$491 -> q$489(app(t,b)) [negative chaining of 102 from 199] 273 + q$490,q$487,q$492,q$493,q$495 -> [negative chaining of 80 from 254] 275 + q$481 -> s$4=x,q$480(app(s$4,u)) [negative chaining of 115 from 203] 276 + q$481 -> s$4=t,q$477(abs(s$4)) [negative chaining of 114 from 255] 278 + q$481 -> s$4=t,q$475(app(s$4,u)) [negative chaining of 114 from 257] 279 + q$495,q$473(app(b,t)) [negative chaining of 63 from 258] 280 + A=abs(x),q$477(A) -> q$490 {[conj([A>=abs(x)],[],[])]} [negative chaining of 108 from 170] 281 + A=app(x,u),q$475(A) -> q$487 {[conj([A>=app(x,u)],[],[])]} [negative chaining of 117 from 176] 284 + q$492,q$495 -> q$491,q$494 [negative chaining of 77 from 253] 286 + q$481,q$477(abs(s$4)) -> s$4=x,q$490 [negative chaining of 259 from 170] 290 + eta(x,A) -> q$486(app(u,A)) [negative chaining of 29 from 94] 292 + eta(s,A) -> q$482(app(b,A)) [negative chaining of 29 from 112] 294 + eta(t,A) -> q$479(app(u,A)) [negative chaining of 29 from 121] 295 + eta(a,A) -> q$476(app(t,A)) [negative chaining of 29 from 175] 304 + q$481 -> s$4=x,q$486(app(u,s$4)) [negative chaining of 115 from 290] 306 + q$499,q$482(app(b,t)) [negative chaining of 43 from 292] 307 + q$485 -> q$482(app(b,t)) [negative chaining of 98 from 292] 308 + q$491 -> q$482(app(b,t)) [negative chaining of 102 from 292] 312 + q$481 -> s$4=t,q$479(app(u,s$4)) [negative chaining of 114 from 294] 313 + q$495,q$476(app(t,b)) [negative chaining of 63 from 295] 315 + q$481,abs(s$4)=abs(x) -> s$4=t,q$490 [negative chaining of 276 from 280] 316 + q$481,q$475(app(s$4,u)) -> s$4=x,q$487 [negative chaining of 275 from 176] 318 + q$481,app(s$4,u)=app(x,u) -> s$4=t,q$487 [negative chaining of 278 from 281] 319 + q$481,q$479(app(u,s$4)) -> s$4=x,q$493 [negative chaining of 304 from 119] 323 + abs(s$4)=abs(t),q$481 -> s$4=x,q$490 [negative chaining of 171 from 286] 324 + q$481,q$481 -> s$4=t,s$4=x,q$490 [negative chaining of 276 from 286] 329 + free(t,0),q$485,q$485 -> [negative chaining of 207 from 139] 343 + q$485,q$489(A),q$476(A),q$473(app(b,t)) -> q$495 {[conj([app(b,t)>A],[],[])]} [negative chaining of 307 from 226] 344 + q$491,q$489(A),q$476(A),q$473(app(b,t)) -> q$495 {[conj([app(b,t)>A],[],[])]} [negative chaining of 308 from 226] 347 + q$489(A),q$476(A),q$473(app(b,t)) -> q$499,q$495 {[conj([app(b,t)>A],[],[])]} [negative chaining of 306 from 226] 352 + q$481 -> s$4=t,s$4=x,q$490 [condensement of 324] 355 + free(t,0),q$485 -> [condensement of 329] 361 + q$481,app(u,s$4)=app(u,x) -> s$4=t,q$493 [negative chaining of 312 from 194] 362 + app(s$4,u)=app(t,u),q$481 -> s$4=x,q$487 [negative chaining of 177 from 316] 363 + q$481,q$481 -> s$4=t,s$4=x,q$487 [negative chaining of 278 from 316] 364 + app(u,s$4)=app(u,t),q$481 -> s$4=x,q$493 [negative chaining of 120 from 319] 365 + q$481,q$481 -> s$4=t,s$4=x,q$493 [negative chaining of 312 from 319] 377 + q$481,q$481 -> q$490,s$4=t,s$4=t,q$490 [negative chaining of 352 from 315] 383 + q$481 -> s$4=t,s$4=x,q$487 [condensement of 363] 384 + q$481 -> s$4=t,s$4=x,q$493 [condensement of 365] 396 + q$481 -> s$4=t,q$490 [condensement of 377] 420 + q$481,q$481 -> q$490,s$4=x,q$490 [negative chaining of 396 from 323] 444 + q$481 -> s$4=x,q$490 [condensement of 420] 445 + q$481 -> q$490,t=x [reduction of 444 by [396]] 454 + q$481 -> q$490,q$483(abs(t)) [negative chaining of 445 from 108] 575 + q$481,q$477(abs(t)) -> q$490,q$490 [negative chaining of 454 from 170] 583 + q$481,q$477(abs(t)) -> q$490 [condensement of 575] 589 + q$481 -> q$490 [negative chaining of 171 from 583] 623 + q$481,q$481 -> q$487,s$4=t,s$4=t,q$487 [negative chaining of 383 from 318] 646 + q$481 -> s$4=t,q$487 [condensement of 623] 671 + q$481,q$481 -> q$487,s$4=x,q$487 [negative chaining of 646 from 362] 698 + q$481 -> s$4=x,q$487 [condensement of 671] 699 + q$481 -> q$487,t=x [reduction of 698 by [646]] 707 + q$481 -> q$487,q$480(app(t,u)) [negative chaining of 699 from 117] 729 + q$481,q$475(app(t,u)) -> q$487,q$487 [negative chaining of 707 from 176] 751 + q$481,q$481 -> q$493,s$4=t,s$4=t,q$493 [negative chaining of 384 from 361] 755 + q$481,q$475(app(t,u)) -> q$487 [condensement of 729] 773 + q$481 -> s$4=t,q$493 [condensement of 751] 796 + q$481,q$481 -> q$493,s$4=x,q$493 [negative chaining of 773 from 364] 823 + q$481 -> s$4=x,q$493 [condensement of 796] 824 + q$481 -> q$493,t=x [reduction of 823 by [773]] 827 + q$481 -> q$487 [negative chaining of 177 from 755] 829 + q$481 -> q$493,q$486(app(u,t)) [negative chaining of 824 from 93] 853 + q$481,q$479(app(u,t)) -> q$493,q$493 [negative chaining of 829 from 119] 881 + eta(s,A) -> q$478(subst(A,0,u)) [negative chaining of 40 from 169] 884 + q$481,q$479(app(u,t)) -> q$493 [condensement of 853] 898 + eta(s,A) -> q$478(subst(A,0,u)) [totality resolution from 881] 916 + q$481 -> q$493 [negative chaining of 120 from 884] 919 + q$485 -> q$478(subst(t,0,u)) [negative chaining of 98 from 898] 929 + q$485,q$474(subst(t,0,u)) -> q$484 [negative chaining of 919 from 223] 965 + q$489(A),q$485,q$476(A) -> q$495,q$495 {[conj([app(b,t)>A],[],[])]} [negative chaining of 279 from 343] 966 + q$489(A),q$476(A),q$491 -> q$495,q$495 {[conj([app(b,t)>A],[],[])]} [negative chaining of 279 from 344] 1002 + q$489(A),q$485,q$476(A) -> q$495 {[conj([app(b,t)>A],[],[])]} [condensement of 965] 1003 + q$489(A),q$476(A),q$491 -> q$495 {[conj([app(b,t)>A],[],[])]} [condensement of 966] 1033 + q$485,q$485,q$476(app(t,b)) -> q$495 [negative chaining of 262 from 1002] 1044 + q$485,q$476(app(t,b)) -> q$495 [condensement of 1033] 1046 + q$485 -> q$495,q$495 [negative chaining of 313 from 1044] 1049 + q$491,q$476(app(t,b)),q$491 -> q$495 [negative chaining of 263 from 1003] 1057 + q$485 -> q$495 [condensement of 1046] 1058 + q$476(app(t,b)),q$491 -> q$495 [condensement of 1049] 1060 + q$485,q$487,q$490,q$492,q$493 -> [negative chaining of 1057 from 273] 1063 + q$485,q$492 -> q$491,q$494 [negative chaining of 1057 from 284] 1067 + q$481,q$485,q$487,q$490,q$492 -> [negative chaining of 916 from 1060] 1069 + q$491 -> q$495,q$495 [negative chaining of 313 from 1058] 1074 + q$491 -> q$495 [condensement of 1069] 1078 + q$484,q$481,q$485,q$487,q$490 -> [negative chaining of 99 from 1067] 1091 + q$481,q$481,q$484,q$485,q$487 -> [negative chaining of 589 from 1078] 1102 + q$481,q$484,q$485,q$487 -> [condensement of 1091] 1104 + q$481,q$481,q$484,q$485 -> [negative chaining of 827 from 1102] 1119 + q$481,q$484,q$485 -> [condensement of 1104] 1123 + q$485,q$492 -> q$491,q$488 [negative chaining of 1063 from 86] 1154 + q$485,q$492 -> q$488 [reduction of 1123 by [140,L]] 1179 + q$484,q$485 -> q$488 [negative chaining of 99 from 1154] 1203 + q$484,q$485 -> [reduction of 1179 by [113,1119,L,L]] 1313 + q$489(A),q$476(A) -> q$495,q$499,q$495 {[conj([app(b,t)>A],[],[])]} [negative chaining of 279 from 347] 1335 + q$489(A),q$476(A) -> q$499,q$495 {[conj([app(b,t)>A],[],[])]} [condensement of 1313] 1353 + q$476(app(t,b)) -> q$499,q$499,q$495 [negative chaining of 261 from 1335] 1357 + q$476(app(t,b)) -> q$499,q$495 [condensement of 1353] 1359 + q$495,q$499,q$495 [negative chaining of 313 from 1357] 1366 + q$499,q$495 [condensement of 1359] 1367 + q$492,q$496,q$498 -> q$495 [negative chaining of 1366 from 74] 1375 + q$492,q$496 -> q$495 [negative chaining of 60 from 1367] 1380 + q$492 -> q$491,q$495 [negative chaining of 77 from 1375] 1387 + q$492 -> q$495 [reduction of 1380 by [1074,L]] 1388 + q$492,q$487,q$490,q$492,q$493 -> [negative chaining of 1387 from 273] 1391 + q$492,q$492 -> q$491,q$494 [negative chaining of 1387 from 284] 1394 + q$487,q$490,q$492,q$493 -> [condensement of 1388] 1397 + q$492 -> q$491,q$494 [condensement of 1391] 1401 + q$481,q$487,q$490,q$492 -> [negative chaining of 916 from 1394] 1415 + q$481,q$487,q$490 -> q$485 [negative chaining of 96 from 1401] 1419 + q$492 -> q$491,q$488 [negative chaining of 1397 from 86] 1438 + q$492 -> q$488 [reduction of 1419 by [140,L]] 1452 + q$485,q$488 [negative chaining of 96 from 1438] 1458 + q$481,q$481,q$487 -> q$485 [negative chaining of 589 from 1415] 1483 + q$481,q$487 -> q$485 [condensement of 1458] 1501 + q$485,q$481 [negative chaining of 1452 from 113] 1503 + q$481,q$481 -> q$485 [negative chaining of 827 from 1483] 1562 + q$481 -> q$485 [condensement of 1503] 1606 + free(t,0),q$474(subst(t,0,A)) [negative chaining of 30 from 225] 1664 + q$485 -> q$474(subst(t,0,A)) {[conj([free(t,0)>A],[],[])]} [negative chaining of 1606 from 355] 1672 + q$485,q$485 -> q$484 [negative chaining of 1664 from 929] 1684 + q$485 -> q$484 [condensement of 1672] 1685 + q$485 -> [reduction of 1684 by [1203,L]] 1699 + q$481 -> [reduction of 1562 by [1685,L]] 1700 + false [reduction of 1501 by [1685,L,1699,L]] Length = 239, Depth = 34 Total time: 92050 milliseconds Number of forward inferences: 990 Number of tableau inferences: 145 Number of generated clauses: 1700 Number of kept clauses: 571 */ /* 20021017 :-sarp(+[15]),saci([2]). Proof: ====== 26 : ~free(A,0) -> eta(abs(app(A,var(0))),subst(A,0,B)) [input] 27 : eta(A,B) -> eta(app(A,C),app(B,C)) [input] 28 : eta(A,B) -> eta(app(C,A),app(C,B)) [input] 29 : eta(A,B) -> eta(abs(A),abs(B)) [input] 30 : 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] 31 : lemmaE2(A,B,C,D)==(0=eta(subst(A,D,C),subst(B,D,C))) [input] 32 : lemmaE1(A,B,C)==(0=free(B,C)<=>free(A,C)) [input] 33 : lemmaE1(A,B,C) [input] 34 : lemmaE2(A,B,C,D) [input] 35 + ~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] 42 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0) [reduction of 26 by [L]] 43 : 0=free(C,A)<=>free(B,A) [reduction of 33 by [32]] 44 : 0= free(C,A)==free(B,A) [condensement of 43] 45 : 0=eta(subst(B,A,D),subst(C,A,D)) [reduction of 34 by [31]] 46 : 0= eta(subst(B,A,D),subst(C,A,D)) [condensement of 45] 47 + 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 35 by [30,L,L,30,30,30,30,30,30,30,30]] 48 : eta(A,B) -> free(B,0)==free(A,0) [reflexivity resolution from 44] 49 : eta(A,B) -> eta(subst(A,0,C),subst(B,0,C)) [reflexivity resolution from 46] 50 + q$499,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 47] 51 + q$499,eta(s,t) [expansion from 47] 52 + 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)))),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(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 47] 51 + q$499,eta(s,t) [expansion from 47] 52 + 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)))),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)))) -> q$499 [expansion from 47] 53 + 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)))) -> q$499 [reduction of 52 by [28,51,L,27,51,L,51,L,28,51,L,27,51,L]] 54 + q$498,q$499,~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)) -> [expansion from 50] 55 + q$498,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 50] 56 + 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))) -> q$498 [expansion from 50] 57 + q$497,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)))) -> q$499 [expansion from 53] 58 + q$497,eta(s,x)and(eta(s,x)=>?A.((A=t or eta(t,A))and(A=x or eta(x,A)))) [expansion from 53] 59 + 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))) -> q$497 [expansion from 53] 60 + q$496,q$498,q$499,~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))) -> [expansion from 54] 61 + q$496,~free(s,0) [expansion from 54] 62 + eta(abs(app(s,var(0))),subst(s,0,u))=>?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> q$496 [expansion from 54] 63 + free(s,0) -> q$496 [reduction of 61 by [L]] 64 + ?A.(A=subst(s,0,u)or eta(subst(s,0,u),A)) -> q$496 [reduction of 62 by [42,63,L,L]] 65 + A=subst(s,0,u)or eta(subst(s,0,u),A) -> q$496 [condensement of 64] 66 + q$498,eta(s,t)and eta(s,x) [expansion from 55] 67 + eta(s,t),eta(s,x) -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))),q$498 [expansion from 55] 69 + A=abs(t)or eta(abs(t),A),A=abs(x)or eta(abs(x),A) -> q$498 [expansion from 56] 70 + q$497 -> q$499,eta(a,b) [expansion from 57] 71 + 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))),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))),q$497 -> q$499 [expansion from 57] 72 + q$497,eta(s,x) [expansion from 58] 73 + eta(s,x) -> ?A.((A=t or eta(t,A))and(A=x or eta(x,A))),q$497 [expansion from 58] 74 + q$495,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))) -> q$497 [expansion from 59] 76 + A=app(u,t)or eta(app(u,t),A),A=app(u,x)or eta(app(u,x),A) -> q$495 [expansion from 59] 77 + ?A.((A=app(t,a)or eta(app(t,a),A))and(A=app(s,b)or eta(app(s,b),A))),q$497,?B.((B=app(a,t)or eta(app(a,t),B))and(B=app(b,s)or eta(app(b,s),B))) -> q$499 [reduction of 71 by [28,70,L,27,70,L]] 78 + 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),q$497 -> q$499 [condensement of 77] 79 + q$497,?A.((A=t or eta(t,A))and(A=x or eta(x,A))) [reduction of 73 by [72]] 80 + q$495,?A.((A=app(t,u)or eta(app(t,u),A))and(A=app(x,u)or eta(app(x,u),A))) -> q$497 [reduction of 74 by [27,72,L]] 81 + A=app(t,u)or eta(app(t,u),A),A=app(x,u)or eta(app(x,u),A),q$495 -> q$497 [condensement of 80] 82 + q$496,q$498,q$499 -> ~free(s,0)and eta(s,t) [expansion from 60] 83 + q$496,q$498,q$499,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))) -> [expansion from 60] 84 + A=subst(s,0,u) -> q$496 [expansion from 65] 86 + q$498,eta(s,t) [expansion from 66] 87 + q$498,eta(s,x) [expansion from 66] 88 + eta(s,t),eta(s,x) -> q$498,(s$2=t or eta(t,s$2))and(s$2=x or eta(x,s$2)) [expansion from 67] 92 + q$494(A),A=abs(t)or eta(abs(t),A) -> q$498 [expansion from 69] 93 + A=abs(x) -> q$494(A) [expansion from 69] 94 + eta(abs(x),A) -> q$494(A) [expansion from 69] 95 + (s$2=t or eta(t,s$2))and(s$2=x or eta(x,s$2)),q$498 [reduction of 88 by [86,87]] 97 + 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))),q$499,q$498 -> [reduction of 83 by [84]] 98 + q$499,q$498 -> ~free(s,0)and eta(s,t) [reduction of 82 by [84]] 99 + q$493(A),q$497,B=app(t,a)or eta(app(t,a),B),A=app(b,s)or eta(app(b,s),A),B=app(s,b)or eta(app(s,b),B) -> q$499 [expansion from 78] 101 + eta(app(a,t),A) -> q$493(A) [expansion from 78] 102 + q$497,(s$3=t or eta(t,s$3))and(s$3=x or eta(x,s$3)) [expansion from 79] 104 + q$492(A),q$495,A=app(x,u)or eta(app(x,u),A) -> q$497 [expansion from 81] 105 + A=app(t,u) -> q$492(A) [expansion from 81] 106 + eta(app(t,u),A) -> q$492(A) [expansion from 81] 107 + q$491(A),A=app(u,t)or eta(app(u,t),A) -> q$495 [expansion from 76] 108 + A=app(u,x) -> q$491(A) [expansion from 76] 109 + eta(app(u,x),A) -> q$491(A) [expansion from 76] 110 + s$2=t,eta(t,s$2),q$498 [expansion from 95] 111 + s$2=x,eta(x,s$2),q$498 [expansion from 95] 112 + q$490(A),q$494(A) -> q$498 [expansion from 92] 113 + A=abs(t) -> q$490(A) [expansion from 92] 114 + eta(abs(t),A) -> q$490(A) [expansion from 92] 115 + q$494(abs(x)) [reflexivity resolution from 93] 117 + 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),q$499,q$498 -> [expansion from 97] 118 + q$498,q$499 -> ~free(s,0) [expansion from 98] 119 + q$498,q$499 -> eta(s,t) [expansion from 98] 120 + q$489(A),q$493(B),q$497,A=app(s,b)or eta(app(s,b),A),B=app(b,s)or eta(app(b,s),B) -> q$499 [expansion from 99] 122 + eta(app(t,a),A) -> q$489(A) [expansion from 99] 123 + q$498,q$499,free(s,0) -> [reduction of 118 by [L]] 124 + eta(s,t) [reduction of 119 by [86,51]] 126 + s$3=t,eta(t,s$3),q$497 [expansion from 102] 127 + s$3=x,eta(x,s$3),q$497 [expansion from 102] 128 + q$488(A),q$492(A),q$495 -> q$497 [expansion from 104] 129 + A=app(x,u) -> q$488(A) [expansion from 104] 130 + eta(app(x,u),A) -> q$488(A) [expansion from 104] 131 + q$492(app(t,u)) [reflexivity resolution from 105] 132 + q$487(A),q$491(A) -> q$495 [expansion from 107] 133 + A=app(u,t) -> q$487(A) [expansion from 107] 134 + eta(app(u,t),A) -> q$487(A) [expansion from 107] 135 + q$491(app(u,x)) [reflexivity resolution from 108] 136 + q$490(abs(t)) [reflexivity resolution from 113] 139 + q$486(A),q$498,q$499,A=subst(s,0,u)or eta(subst(s,0,u),A) -> [expansion from 117] 141 + eta(abs(app(t,var(0))),A) -> q$486(A) [expansion from 117] 142 + q$485(A),q$493(A),q$489(B),q$497,B=app(s,b)or eta(app(s,b),B) -> q$499 [expansion from 120] 144 + eta(app(b,s),A) -> q$485(A) [expansion from 120] 146 + q$488(app(x,u)) [reflexivity resolution from 129] 147 + q$487(app(u,t)) [reflexivity resolution from 133] 148 + q$484(A),q$486(A),q$499,q$498 -> [expansion from 139] 150 + eta(subst(s,0,u),A) -> q$484(A) [expansion from 139] 152 + q$483(A),q$489(A),q$485(B),q$493(B),q$497 -> q$499 [expansion from 142] 154 + eta(app(s,b),A) -> q$483(A) [expansion from 142] 159 + q$494(abs(t)) -> q$498 [negative chaining of 136 from 112] 160 + q$491(app(u,t)) -> q$495 [negative chaining of 147 from 132] 164 + q$492(app(x,u)),q$495 -> q$497 [negative chaining of 146 from 128] 175 + free(t,0)==free(s,0) [negative chaining of 124 from 48] 189 + q$499,q$498,free(t,0) -> [reduction of 123 by [175]] 196 + eta(x,A) -> q$494(abs(A)) [negative chaining of 29 from 94] 197 + eta(t,A) -> q$490(abs(A)) [negative chaining of 29 from 114] 205 + q$498,s$2=x,q$494(abs(s$2)) [negative chaining of 111 from 196] 207 + q$498,s$2=t,q$490(abs(s$2)) [negative chaining of 110 from 197] 210 + eta(a,A) -> q$493(app(A,t)) [negative chaining of 27 from 101] 211 + eta(t,A) -> q$492(app(A,u)) [negative chaining of 27 from 106] 214 + eta(x,A) -> q$488(app(A,u)) [negative chaining of 27 from 130] 217 + eta(s,A) -> q$483(app(A,b)) [negative chaining of 27 from 154] 222 + q$497 -> q$499,q$493(app(b,t)) [negative chaining of 70 from 210] 224 + q$497,s$3=t,q$492(app(s$3,u)) [negative chaining of 126 from 211] 228 + q$497,s$3=x,q$488(app(s$3,u)) [negative chaining of 127 from 214] 229 + q$483(app(t,b)) [negative chaining of 124 from 217] 235 + q$494(abs(s$2)) -> q$498,s$2=t,q$498 [negative chaining of 207 from 112] 242 + q$492(app(s$3,u)),q$495 -> q$497,s$3=x,q$497 [negative chaining of 228 from 128] 249 + eta(x,A) -> q$491(app(u,A)) [negative chaining of 28 from 109] 250 + eta(a,A) -> q$489(app(t,A)) [negative chaining of 28 from 122] 252 + eta(t,A) -> q$487(app(u,A)) [negative chaining of 28 from 134] 253 + eta(s,A) -> q$485(app(b,A)) [negative chaining of 28 from 144] 259 + q$494(abs(s$2)) -> s$2=t,q$498 [condensement of 235] 265 + q$492(app(s$3,u)),q$495 -> s$3=x,q$497 [condensement of 242] 272 + q$497,s$3=x,q$491(app(u,s$3)) [negative chaining of 127 from 249] 273 + q$497 -> q$499,q$489(app(t,b)) [negative chaining of 70 from 250] 275 + q$497,s$3=t,q$487(app(u,s$3)) [negative chaining of 126 from 252] 276 + q$485(app(b,t)) [negative chaining of 124 from 253] 281 + q$483(A),q$493(app(b,t)),q$489(A),q$497 -> q$499 [negative chaining of 276 from 152] 284 + q$498,s$2=x,s$2=t,q$498 [negative chaining of 205 from 259] 289 + q$491(app(u,s$3)) -> q$497,s$3=t,q$495 [negative chaining of 275 from 132] 291 + q$495 -> q$497,s$3=t,s$3=x,q$497 [negative chaining of 224 from 265] 292 + eta(s,A) -> q$484(subst(A,0,u)) [negative chaining of 49 from 150] 307 + s$2=x,s$2=t,q$498 [condensement of 284] 313 + q$495 -> s$3=t,s$3=x,q$497 [condensement of 291] 320 + eta(t,x),s$2=t,q$498,q$498,s$2=t [chaining of 307 from 110] 337 + eta(t,x),q$498,s$2=t [condensement of 320] 379 + q$495 -> eta(t,x),q$497,s$3=t,q$497,s$3=t [chaining of 313 from 126] 393 + q$495 -> eta(t,x),q$497,s$3=t [condensement of 379] 394 + q$495 -> s$3=t,q$497 [reduction of 393 by [211,164,L,L]] 419 + q$492(app(t,u)),q$495,q$495 -> q$497,s$3=x,q$497 [negative chaining of 394 from 265] 437 + q$492(app(t,u)),q$495 -> s$3=x,q$497 [condensement of 419] 438 + q$492(app(t,u)),q$495 -> q$497,t=x [reduction of 437 by [394]] 442 + eta(x,t),q$498,eta(t,x),q$498,s$2=x [chaining of 337 from 111] 455 + eta(x,t),eta(t,x),q$498,s$2=x [condensement of 442] 456 + eta(t,x),q$498,t=x [reduction of 455 by [196,159,L,L,337]] 469 + q$498,x=t,q$490(abs(x)) [negative chaining of 456 from 197] 474 + q$484(subst(t,0,u)) [negative chaining of 124 from 292] 477 + q$486(subst(t,0,u)),q$498,q$499 -> [negative chaining of 474 from 148] 479 + q$494(abs(x)) -> q$498,x=t,q$498 [negative chaining of 469 from 112] 494 + q$494(abs(x)) -> x=t,q$498 [condensement of 479] 509 + x=t,q$498 [negative chaining of 115 from 494] 514 + q$494(abs(t)),q$498 [chaining of 509 from 115] 546 + q$498 [reduction of 514 by [159,L]] 558 + free(t,0),q$499 -> [reduction of 189 by [546]] 560 + q$486(subst(t,0,u)),q$499 -> [reduction of 477 by [546]] 565 + q$497,s$3=x,q$497,s$3=t,q$495 [negative chaining of 272 from 289] 567 + q$495 -> q$497,x=t [negative chaining of 131 from 438] 568 + free(t,0),q$486(subst(t,0,A)) [negative chaining of 42 from 141] 575 + s$3=x,q$497,s$3=t,q$495 [condensement of 565] 576 + s$3=x,q$497,s$3=t [reduction of 575 by [394,L]] 588 + eta(t,x),q$497,s$3=t,q$497,s$3=t [chaining of 576 from 126] 604 + eta(t,x),q$497,s$3=t [condensement of 588] 630 + q$492(app(t,u)),q$495,q$495 -> q$497,q$497 [negative chaining of 567 from 164] 641 + q$492(app(t,u)),q$495 -> q$497 [condensement of 630] 649 + eta(x,t),q$497,eta(t,x),q$497,s$3=x [chaining of 604 from 127] 664 + eta(x,t),eta(t,x),q$497,s$3=x [condensement of 649] 665 + t=x,q$497,eta(t,x) [reduction of 664 by [604,249,160,567,L,L,L]] 683 + q$497,x=t,q$487(app(u,x)) [negative chaining of 665 from 252] 686 + q$499 -> q$486(subst(t,0,A)) {[conj([free(t,0)>A],[],[])]} [negative chaining of 568 from 558] 689 + q$495 -> q$497 [negative chaining of 131 from 641] 694 + q$491(app(u,x)) -> q$497,x=t,q$495 [negative chaining of 683 from 132] 697 + q$497,q$483(A),q$489(A),q$497 -> q$499,q$499 [negative chaining of 222 from 281] 712 + q$491(app(u,x)) -> q$497,x=t [reduction of 694 by [689,L]] 714 + q$483(A),q$489(A),q$497 -> q$499 [condensement of 697] 719 + q$497,x=t [negative chaining of 135 from 712] 721 + q$489(app(t,b)),q$497 -> q$499 [negative chaining of 229 from 714] 736 + q$497 -> q$499 [reduction of 273 by [721,L]] 745 + q$491(app(u,t)),q$497 [chaining of 719 from 135] 759 + q$497 [reduction of 745 by [160,689,L,L]] 768 + q$499 [reduction of 736 by [759]] 772 + q$486(subst(t,0,u)) -> [reduction of 560 by [768]] 773 + q$486(subst(t,0,A)) {[conj([free(t,0)>A],[],[])]} [reduction of 686 by [768]] 780 + false [negative chaining of 773 from 772] Length = 188, Depth = 34, Search Depth = 4 Total time: 45997 milliseconds Number of forward inferences: 382 Number of tableau inferences: 101 Number of generated clauses: 783 Number of kept clauses: 332 */