use(subst).
use(int).
use(eta).
use(subst_lemmas).
use(lemmaE2).
use(lemmaF2).
use(lemmaF3).

lemmaF2(S,K,I).
lemmaF3(S,T,K,I).
lemma5(T,U,V,I,J).

goal

%Induktionsanfang der Induktion ueber eta

(~free(s,0) =>
  lemmaE2(abs(app(s,var(0))),subst(s,0,a),b,i)),

%Die drei Induktionsschritte

((eta(s,t) and all(I,lemmaE2(s,t,u,I))) =>
  lemmaE2(app(s,v),app(t,v),u,k) and lemmaE2(app(v,s),app(v,t),u,k)),

((eta(s,t) and all(I,all(U,lemmaE2(s,t,U,I)))) =>
  lemmaE2(abs(s),abs(t),u,l)) -> [].

top_predicates_precedence([lemmaE2,lemmaF2,lemmaF3,lemma5]).
option([var_overlaps(off),search_depth(0)]).
:-sama([]),saci([2]).

/*
Proof:
======

  11 : A<s(A)                                                           [input]
  16 : A<B -> subst(var(A),B,C)=var(A)                                  [input]
  17 : subst(app(A,B),C,D)=app(subst(A,C,D),subst(B,C,D))               [input]
  18 : subst(abs(A),B,C)=abs(subst(A,s(B),lift(C,0)))                   [input]
  36 : A<s(A)                                                           [input]
  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]
  50 : lemma5(A,B,C,D,E)==(D<s(E)and 0=<D=>subst(subst(A,s(E),lift(C,D)),D,subst(B,E,C))=subst(subst(A,D,B),E,C)) [input]
  53 : lemmaE2(A,B,C,D)==(0=<D and eta(A,B)=>eta(subst(A,D,C),subst(B,D,C))) [input]
  54 : lemmaF2(A,B,C)==(0=<B and 0=<C=>free(lift(A,B),C)<=>free(A,p(C))and B<C or free(A,C)and C<B) [input]
  55 : lemmaF3(A,B,C,D)==(0=<D and 0=<C=>free(subst(A,C,B),D)<=>free(A,C)and free(B,D)or(D<C and free(A,D)or C=<D and free(A,s(D)))) [input]
  56 : lemmaF2(A,B,C)                                                   [input]
  57 : lemmaF3(A,B,C,D)                                                 [input]
  58 : lemma5(A,B,C,D,E)                                                [input]
  59 + ~free(s,0)=>lemmaE2(abs(app(s,var(0))),subst(s,0,a),b,i),eta(s,t)and!A.(lemmaE2(s,t,u,A))=>lemmaE2(app(s,v),app(t,v),u,k)and lemmaE2(app(v,s),app(v,t),u,k),eta(s,t)and!B,C.(lemmaE2(s,t,C,B))=>lemmaE2(abs(s),abs(t),u,l) ->  [input]
  63 : A=<B,subst(var(B),A,C)=var(B)              [totality resolution from 16]
  70 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0)       [expansion from 39]
  72 : 0=<A and 0=<B=>free(lift(C,A),B)<=>free(C,p(B))and A<B or free(C,B)and B<A [reduction of 56 by [54]]
  73 : 0=<A,0=<B -> free(lift(C,A),B)==(free(C,p(B))and A<B or free(C,B)and B<A) [expansion from 72]
  75 : A<0,B<0,free(lift(C,B),A)==(free(C,p(A))and B<A or free(C,A)and A<B) [totality resolution from 73]
  76 : 0=<A and 0=<B=>free(subst(C,B,D),A)<=>free(C,B)and free(D,A)or(A<B and free(C,A)or B=<A and free(C,s(A))) [reduction of 57 by [55]]
  77 : 0=<A,0=<B -> free(subst(C,B,D),A)==(free(C,B)and free(D,A)or(A<B and free(C,A)or B=<A and free(C,s(A)))) [expansion from 76]
  79 : A<0,B<0,free(subst(C,A,D),B)==(free(C,A)and free(D,B)or(B<A and free(C,B)or A=<B and free(C,s(B)))) [totality resolution from 77]
  80 : A<s(B)and 0=<A=>subst(subst(C,s(B),lift(D,A)),A,subst(E,B,D))=subst(subst(C,A,E),B,D) [reduction of 58 by [50]]
  81 : A<s(B),0=<A -> subst(subst(C,s(B),lift(D,A)),A,subst(E,B,D))=subst(subst(C,A,E),B,D) [expansion from 80]
  83 : A<0,s(B)=<A,subst(subst(C,s(B),lift(D,A)),A,subst(E,B,D))=subst(subst(C,A,E),B,D) [totality resolution from 81]
  84 + eta(s,t)and!A.(0=<A and eta(s,t)=>eta(subst(s,A,u),subst(t,A,u)))=>(0=<k and eta(app(s,v),app(t,v))=>eta(app(subst(s,k,u),subst(v,k,u)),app(subst(t,k,u),subst(v,k,u))))and(0=<k and eta(app(v,s),app(v,t))=>eta(app(subst(v,k,u),subst(s,k,u)),app(subst(v,k,u),subst(t,k,u)))),~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)),eta(s,t)and!B,C.(0=<B and eta(s,t)=>eta(subst(s,B,C),subst(t,B,C)))=>0=<l and eta(abs(s),abs(t))=>eta(abs(subst(s,s(l),lift(u,0))),abs(subst(t,s(l),lift(u,0)))) ->  [reduction of 59 by [53,18,17,53,17,17,53,17,17,53,53,18,18,53]]
  85 + p$499,~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)),eta(s,t)and!A,B.(0=<A and eta(s,t)=>eta(subst(s,A,B),subst(t,A,B)))=>0=<l and eta(abs(s),abs(t))=>eta(abs(subst(s,s(l),lift(u,0))),abs(subst(t,s(l),lift(u,0)))) ->  [expansion from 84]
  86 + p$499,eta(s,t)and!A.(0=<A and eta(s,t)=>eta(subst(s,A,u),subst(t,A,u))) [expansion from 84]
  87 + (0=<k and eta(app(s,v),app(t,v))=>eta(app(subst(s,k,u),subst(v,k,u)),app(subst(t,k,u),subst(v,k,u))))and(0=<k and eta(app(v,s),app(v,t))=>eta(app(subst(v,k,u),subst(s,k,u)),app(subst(v,k,u),subst(t,k,u)))) -> p$499 [expansion from 84]
  88 + 0=<k and eta(app(s,v),app(t,v))=>eta(app(subst(s,k,u),subst(v,k,u)),app(subst(t,k,u),subst(v,k,u))),0=<k and eta(app(v,s),app(v,t))=>eta(app(subst(v,k,u),subst(s,k,u)),app(subst(v,k,u),subst(t,k,u))) -> p$499 [expansion from 87]
  89 + p$498,~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)),p$499 ->  [expansion from 85]
  90 + p$498,eta(s,t)and!A,B.(0=<A and eta(s,t)=>eta(subst(s,A,B),subst(t,A,B))) [expansion from 85]
  91 + 0=<l and eta(abs(s),abs(t))=>eta(abs(subst(s,s(l),lift(u,0))),abs(subst(t,s(l),lift(u,0)))) -> p$498 [expansion from 85]
  92 + p$497,p$499                                          [expansion from 86]
  93 + p$497 -> eta(s,t)                                    [expansion from 86]
  94 + p$497 -> !A.(0=<A and eta(s,t)=>eta(subst(s,A,u),subst(t,A,u))) [expansion from 86]
  95 + p$497,0=<A,eta(s,t) -> eta(subst(s,A,u),subst(t,A,u)) [expansion from 94]
  96 + p$497,eta(s,t) -> A<0,eta(subst(s,A,u),subst(t,A,u)) [totality resolution from 95]
  97 + p$497 -> eta(subst(s,A,u),subst(t,A,u)),A<0    [reduction of 96 by [93]]
  98 + p$496,0=<k and eta(app(s,v),app(t,v))=>eta(app(subst(s,k,u),subst(v,k,u)),app(subst(t,k,u),subst(v,k,u))) -> p$499 [expansion from 88]
  99 + p$496,0=<k and eta(app(v,s),app(v,t))                [expansion from 88]
 100 + eta(app(subst(v,k,u),subst(s,k,u)),app(subst(v,k,u),subst(t,k,u))) -> p$496 [expansion from 88]
 101 + p$495,p$498                                          [expansion from 90]
 102 + p$495 -> eta(s,t)                                    [expansion from 90]
 103 + p$495 -> !A,B.(0=<A and eta(s,t)=>eta(subst(s,A,B),subst(t,A,B))) [expansion from 90]
 104 + p$495,0=<A,eta(s,t) -> eta(subst(s,A,B),subst(t,A,B)) [expansion from 103]
 105 + p$495,eta(s,t) -> A<0,eta(subst(s,A,B),subst(t,A,B)) [totality resolution from 104]
 106 + p$495 -> eta(subst(s,A,B),subst(t,A,B)),A<0  [reduction of 105 by [102]]
 107 + p$494 -> p$498                                       [expansion from 91]
 108 + p$494,0=<l and eta(abs(s),abs(t))                    [expansion from 91]
 109 + eta(abs(subst(s,s(l),lift(u,0))),abs(subst(t,s(l),lift(u,0)))) -> p$494 [expansion from 91]
 110 + p$493,p$496 -> p$499                                 [expansion from 98]
 111 + p$493,0=<k and eta(app(s,v),app(t,v))                [expansion from 98]
 112 + eta(app(subst(s,k,u),subst(v,k,u)),app(subst(t,k,u),subst(v,k,u))) -> p$493 [expansion from 98]
 113 + p$492,p$496                                          [expansion from 99]
 114 + p$492 -> 0=<k                                        [expansion from 99]
 116 + p$491,p$494                                         [expansion from 108]
 117 + p$491 -> 0=<l                                       [expansion from 108]
 119 + p$490,p$493                                         [expansion from 111]
 120 + p$490 -> 0=<k                                       [expansion from 111]
 122 + p$496,0=<k                           [negative chaining of 113 from 114]
 123 + p$494,0=<l                           [negative chaining of 116 from 117]
 124 + p$493,0=<k                           [negative chaining of 119 from 120]
 136 + eta(subst(s,k,u),subst(t,k,u)) -> p$496 [negative chaining of 41 from 100]
 137 + eta(subst(s,k,u),subst(t,k,u)) -> p$493 [negative chaining of 40 from 112]
 142 + p$499,eta(subst(s,A,u),subst(t,A,u)),A<0 [negative chaining of 92 from 97]
 143 + eta(subst(s,s(l),lift(u,0)),subst(t,s(l),lift(u,0))) -> p$494 [negative chaining of 42 from 109]
 144 + p$498,eta(subst(s,A,B),subst(t,A,B)),A<0 [negative chaining of 101 from 106]
 145 + p$499,k<0,p$496                      [negative chaining of 142 from 136]
 146 + p$499,k<0,p$493                      [negative chaining of 142 from 137]
 147 + p$499,p$496                                [reduction of 145 by [122,L]]
 148 + p$499                            [reduction of 146 by [124,L,110,147,L]]
 149 + ~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)),p$498 ->  [reduction of 89 by [148]]
 152 + p$498,s(l)<0,p$494                   [negative chaining of 144 from 143]
 155 + p$498                             [reduction of 152 by [36,123,L,107,L]]
 156 + ~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)) ->  [reduction of 149 by [155]]
 157 + ~free(s,0)                                          [expansion from 156]
 158 + 0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)) ->  [expansion from 156]
 159 + free(s,0) ->                                        [expansion from 157]
 160 + 0=<i=>eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)) ->  [reduction of 158 by [70,159,L,L]]
 161 + 0=<i                                                [expansion from 160]
 162 + eta(abs(app(subst(s,s(i),lift(b,0)),subst(var(0),s(i),lift(b,0)))),subst(subst(s,0,a),i,b)) ->  [expansion from 160]
 168 + eta(abs(app(subst(s,s(i),lift(b,0)),var(0))),subst(subst(s,0,a),i,b)) -> s(i)=<0 [negative chaining of 63 from 162]
 169 + eta(abs(app(subst(s,s(i),lift(b,0)),var(0))),subst(subst(s,0,a),i,b)) -> s(i)=0 [reduction of 168 by [36,161]]
 212 : eta(abs(app(subst(A,s(B),lift(C,0)),var(0))),subst(subst(A,0,D),B,C)),s(B)=<0,free(subst(A,s(B),lift(C,0)),0) [chaining of 83 from 70]
 219 : eta(abs(app(subst(A,s(B),lift(C,0)),var(0))),subst(subst(A,0,D),B,C)),s(B)=<0,free(A,s(B))and(free(C,p(0))and 0<0 or free(C,0)and 0<0)or(0<s(B)and free(A,0)or s(B)=<0 and free(A,s(0))) [reduction of 212 by [79,75]]
 220 : eta(abs(app(subst(A,s(B),lift(C,0)),var(0))),subst(subst(A,0,D),B,C)),s(B)=<0,free(A,s(B))and(free(C,p(0))and 0<0 or free(C,0)and 0<0),0<s(B)and free(A,0),s(B)=<0 and free(A,s(0)) [expansion from 219]
 435 + s(i)=<0,free(s,s(i))and(free(b,p(0))and 0<0 or free(b,0)and 0<0),0<s(i)and free(s,0),s(i)=<0 and free(s,s(0)),s(i)=0 [negative chaining of 220 from 169]
 436 + s(i)=<0,free(s,s(i))and(free(b,p(0))and 0<0 or free(b,0)and 0<0),0<s(i)and free(s,0),s(i)=<0 and free(s,s(0)) [condensement of 435]
 437 + s(i)=0,free(s,s(i))and(free(b,p(0))and 0<0 or free(b,0)and 0<0),s(i)=<0 and free(s,s(0)) [reduction of 436 by [36,161,159,L,L]]
 438 + p$464,s(i)=0,s(i)=<0 and free(s,s(0))               [expansion from 437]
 440 + p$464 -> free(b,p(0))and 0<0 or free(b,0)and 0<0    [expansion from 437]
 441 + p$464 -> free(b,p(0))and 0<0,free(b,0)and 0<0       [expansion from 440]
 442 + p$463,p$464,s(i)=0                                  [expansion from 438]
 443 + p$463 -> s(i)=<0                                    [expansion from 438]
 445 + p$463 -> s(i)=0                           [reduction of 443 by [36,161]]
 446 + i<0,p$464,p$463                                [chaining of 11 from 442]
 499 + p$463,p$464                                [reduction of 446 by [161,L]]
 500 + p$464,s(i)=0                         [negative chaining of 499 from 445]
 502 + i<0,p$464                                      [chaining of 11 from 500]
 555 + p$464                                      [reduction of 502 by [161,L]]
 556 + free(b,0)and 0<0,free(b,p(0))and 0<0         [reduction of 441 by [555]]
 558 + p$462,free(b,0)and 0<0                              [expansion from 556]
 560 + p$462 ->                                            [expansion from 556]
 561 + free(b,0)and 0<0                           [reduction of 558 by [560,L]]
 563 + false                                               [expansion from 561]

Length = 109, Depth = 33



Total time: 31540 milliseconds

Number of forward inferences: 225
Number of tableau inferences: 127
Number of kept clauses: 257
*/