use(subst).
use(int).
use(eta).
use(lemmaE6).
use(lemmaF2).
use(subst_lemmas).

lemma2(T,S,J,I).
lemmaF2(S,K,I).

%Induktionsanfang der Induktion ueber eta

(~free(s,0) => lemmaE6(abs(app(s,var(0))),subst(s,0,u),i)),

%2 Induktionsschritte

((lemmaE6(s,t,i) and eta(s,t)) =>
 (lemmaE6(app(s,u),app(t,u),i) and lemmaE6(app(u,s),app(u,t),i))),

((all(I,lemmaE6(s,t,I)) and eta(s,t)) => lemmaE6(abs(s),abs(t),i)) -> [].

option([var_overlaps(off),search_depth(1)]).
:-sarp(+[15]),saci([2]).

/*
Proof:
======

  11 : A<s(A)                                                           [input]
  19 : A<B -> lift(var(A),B)=var(A)                                     [input]
  21 : lift(app(A,B),C)=app(lift(A,C),lift(B,C))                        [input]
  22 : lift(abs(A),B)=abs(lift(A,s(B)))                                 [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]
  46 : lemmaE6(A,B,C)==(0=<C and eta(A,B)=>eta(lift(A,C),lift(B,C)))    [input]
  47 : 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]
  49 : lemma2(A,B,C,D)==(C<s(D)and 0=<C=>lift(subst(A,C,B),D)=subst(lift(A,s(D)),C,lift(B,D))) [input]
  55 : lemma2(A,B,C,D)                                                  [input]
  56 : lemmaF2(A,B,C)                                                   [input]
  57 : ~free(s,0)=>lemmaE6(abs(app(s,var(0))),subst(s,0,u),i),lemmaE6(s,t,i)and eta(s,t)=>lemmaE6(app(s,u),app(t,u),i)and lemmaE6(app(u,s),app(u,t),i),!A.(lemmaE6(s,t,A)) and eta(s,t)=>lemmaE6(abs(s),abs(t),i) ->  [input]
  62 : A=<B,lift(var(B),A)=var(B)                 [totality resolution from 19]
  68 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0)       [expansion from 39]
  70 : A<s(B)and 0=<A=>lift(subst(C,A,D),B)=subst(lift(C,s(B)),A,lift(D,B)) [reduction of 55 by [49]]
  71 : A<s(B),0=<A -> lift(subst(C,A,D),B)=subst(lift(C,s(B)),A,lift(D,B)) [expansion from 70]
  73 : A<0,s(B)=<A,lift(subst(C,A,D),B)=subst(lift(C,s(B)),A,lift(D,B)) [totality resolution from 71]
  74 : 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 [47]]
  75 : 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 74]
  77 : 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 75]
  78 : (0=<i and eta(s,t)=>eta(lift(s,i),lift(t,i)))and eta(s,t)=>(0=<i and eta(app(s,u),app(t,u))=>eta(app(lift(s,i),lift(u,i)),app(lift(t,i),lift(u,i))))and(0=<i and eta(app(u,s),app(u,t))=>eta(app(lift(u,i),lift(s,i)),app(lift(u,i),lift(t,i)))),~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,u))=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)),!A.(0=<A and eta(s,t)=>eta(lift(s,A),lift(t,A))) and eta(s,t)=>0=<i and eta(abs(s),abs(t))=>eta(abs(lift(s,s(i))),abs(lift(t,s(i)))) ->  [reduction of 57 by [46,22,21,46,21,21,46,21,21,46,46,22,22,46]]
  79 : p$199,~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,u))=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)),(0=<i and eta(s,t)=>eta(lift(s,i),lift(t,i)))and eta(s,t)=>(0=<i and eta(app(s,u),app(t,u))=>eta(app(lift(s,i),lift(u,i)),app(lift(t,i),lift(u,i))))and(0=<i and eta(app(u,s),app(u,t))=>eta(app(lift(u,i),lift(s,i)),app(lift(u,i),lift(t,i)))) ->  [expansion from 78]
  80 : p$199,!A.(0=<A and eta(s,t)=>eta(lift(s,A),lift(t,A))) and eta(s,t) [expansion from 78]
  81 : 0=<i and eta(abs(s),abs(t))=>eta(abs(lift(s,s(i))),abs(lift(t,s(i)))) -> p$199 [expansion from 78]
  82 : p$198,~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,u))=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)),p$199 ->  [expansion from 79]
  83 : p$198,(0=<i and eta(s,t)=>eta(lift(s,i),lift(t,i)))and eta(s,t) [expansion from 79]
  84 : (0=<i and eta(app(s,u),app(t,u))=>eta(app(lift(s,i),lift(u,i)),app(lift(t,i),lift(u,i))))and(0=<i and eta(app(u,s),app(u,t))=>eta(app(lift(u,i),lift(s,i)),app(lift(u,i),lift(t,i)))) -> p$198 [expansion from 79]
  85 : 0=<i and eta(app(s,u),app(t,u))=>eta(app(lift(s,i),lift(u,i)),app(lift(t,i),lift(u,i))),0=<i and eta(app(u,s),app(u,t))=>eta(app(lift(u,i),lift(s,i)),app(lift(u,i),lift(t,i))) -> p$198 [expansion from 84]
  86 : p$197,p$199                                          [expansion from 80]
  87 : p$197 -> !A.(0=<A and eta(s,t)=>eta(lift(s,A),lift(t,A))) [expansion from 80]
  88 : p$197 -> eta(s,t)                                    [expansion from 80]
  89 : p$197,0=<A,eta(s,t) -> eta(lift(s,A),lift(t,A))      [expansion from 87]
  90 : p$197,eta(s,t) -> A<0,eta(lift(s,A),lift(t,A)) [totality resolution from 89]
  91 : p$196 -> p$199                                       [expansion from 81]
  92 : p$196,0=<i and eta(abs(s),abs(t))                    [expansion from 81]
  93 : eta(abs(lift(s,s(i))),abs(lift(t,s(i)))) -> p$196    [expansion from 81]
  94 : p$195,p$198                                          [expansion from 83]
  95 : p$195 -> 0=<i and eta(s,t)=>eta(lift(s,i),lift(t,i)) [expansion from 83]
  96 : p$195 -> eta(s,t)                                    [expansion from 83]
  97 : p$195,0=<i,eta(s,t) -> eta(lift(s,i),lift(t,i))      [expansion from 95]
  98 : p$195,eta(s,t) -> i<0,eta(lift(s,i),lift(t,i)) [totality resolution from 97]
  99 : p$194,0=<i and eta(app(s,u),app(t,u))=>eta(app(lift(s,i),lift(u,i)),app(lift(t,i),lift(u,i))) -> p$198 [expansion from 85]
 100 : p$194,0=<i and eta(app(u,s),app(u,t))                [expansion from 85]
 101 : eta(app(lift(u,i),lift(s,i)),app(lift(u,i),lift(t,i))) -> p$194 [expansion from 85]
 102 : p$193,p$196                                          [expansion from 92]
 103 : p$193 -> 0=<i                                        [expansion from 92]
 105 : p$192,p$194 -> p$198                                 [expansion from 99]
 106 : p$192,0=<i and eta(app(s,u),app(t,u))                [expansion from 99]
 107 : eta(app(lift(s,i),lift(u,i)),app(lift(t,i),lift(u,i))) -> p$192 [expansion from 99]
 108 : p$191,p$194                                         [expansion from 100]
 109 : p$191 -> 0=<i                                       [expansion from 100]
 111 : p$190,p$192                                         [expansion from 106]
 112 : p$190 -> 0=<i                                       [expansion from 106]
 120 : p$196,0=<i                           [negative chaining of 102 from 103]
 121 : p$194,0=<i                           [negative chaining of 108 from 109]
 122 : p$192,0=<i                           [negative chaining of 111 from 112]
 123 : p$199,eta(s,t)                         [negative chaining of 86 from 88]
 124 : p$198,eta(s,t)                         [negative chaining of 94 from 96]
 142 : eta(lift(s,s(i)),lift(t,s(i))) -> p$196 [negative chaining of 42 from 93]
 143 : eta(lift(s,i),lift(t,i)) -> p$194     [negative chaining of 41 from 101]
 144 : eta(lift(s,i),lift(t,i)) -> p$192     [negative chaining of 40 from 107]
 145 : p$197 -> p$199,eta(lift(s,A),lift(t,A)),A<0 [negative chaining of 123 from 90]
 147 : A<0,eta(lift(s,A),lift(t,A)),p$199            [reduction of 145 by [86]]
 148 : p$199,s(i)<0,p$196                   [negative chaining of 147 from 142]
 151 : p$199                              [reduction of 148 by [36,120,L,91,L]]
 152 : ~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,u))=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)),p$198 ->  [reduction of 82 by [151]]
 153 : p$195 -> p$198,eta(lift(s,i),lift(t,i)),i<0 [negative chaining of 124 from 98]
 154 : i<0,eta(lift(s,i),lift(t,i)),p$198            [reduction of 153 by [94]]
 156 : p$198,i<0,p$194                      [negative chaining of 154 from 143]
 157 : p$198,i<0,p$192                      [negative chaining of 154 from 144]
 158 : p$198,p$194                                [reduction of 156 by [121,L]]
 159 : p$198                            [reduction of 157 by [122,L,105,158,L]]
 160 : ~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,u))=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)) ->  [reduction of 152 by [159]]
 161 : ~free(s,0)                                          [expansion from 160]
 162 : 0=<i and eta(abs(app(s,var(0))),subst(s,0,u))=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)) ->  [expansion from 160]
 163 : free(s,0) ->                                        [expansion from 161]
 164 : 0=<i=>eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)) ->  [reduction of 162 by [68,163,L,L]]
 165 : 0=<i                                                [expansion from 164]
 166 : eta(abs(app(lift(s,s(i)),lift(var(0),s(i)))),lift(subst(s,0,u),i)) ->  [expansion from 164]
 181 : eta(abs(app(lift(s,s(i)),var(0))),lift(subst(s,0,u),i)) -> s(i)=<0 [negative chaining of 62 from 166]
 183 : eta(abs(app(lift(s,s(i)),var(0))),lift(subst(s,0,u),i)) -> s(i)=0 [reduction of 181 by [36,165]]
 193 : eta(abs(app(lift(A,s(B)),var(0))),lift(subst(A,0,C),B)),s(B)=<0,free(lift(A,s(B)),0) [chaining of 73 from 68]
 197 : eta(abs(app(lift(A,s(B)),var(0))),lift(subst(A,0,C),B)),s(B)=<0,free(A,p(0))and s(B)<0 or free(A,0)and 0<s(B) [reduction of 193 by [77]]
 198 : eta(abs(app(lift(A,s(B)),var(0))),lift(subst(A,0,C),B)),s(B)=<0,free(A,p(0))and s(B)<0,free(A,0)and 0<s(B) [expansion from 197]
 278 : s(i)=<0,free(s,p(0))and s(i)<0,free(s,0)and 0<s(i),s(i)=0 [negative chaining of 198 from 183]
 279 : s(i)=<0,free(s,p(0))and s(i)<0,free(s,0)and 0<s(i) [condensement of 278]
 280 : s(i)=0,free(s,p(0))and s(i)<0     [reduction of 279 by [36,165,163,L,L]]
 281 : p$180,s(i)=0                                        [expansion from 280]
 283 : p$180 -> s(i)<0                                     [expansion from 280]
 284 : p$180 ->                                [reduction of 283 by [36,165,L]]
 285 : s(i)=0                                     [reduction of 281 by [284,L]]
 289 : i<0                                            [chaining of 11 from 285]
 309 : false                                      [reduction of 289 by [165,L]]

Length = 96, Depth = 27



Total time: 54360 milliseconds

Number of forward inferences: 97
Number of tableau inferences: 66
Number of kept clauses: 183
*/