use(subst).
use(eta).
use(lemmaE1).
use(lemmaF3).

lemmaF3(S,T,K,I).

goal

%Induktionsanfang der Induktion ueber eta

((0=<i and ~free(s,0)) =>
  lemmaE1(abs(app(s,var(0))),subst(s,0,a),i)),

%Die drei Induktionsschritte

((eta(s,t) and lemmaE1(s,t,k)) =>
  lemmaE1(app(s,v),app(t,v),k) and lemmaE1(app(v,s),app(v,t),k)),

((eta(s,t) and 0=<l and all(I,lemmaE1(s,t,I))) =>
  lemmaE1(abs(s),abs(t),l)) -> [].

top_predicates_precedence([lemmaE1,lemmaF3]).

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

/*
Proof:
======

  11 : A<s(A)                                                           [input]
  23 : free(var(A),B)==(A=B)                                            [input]
  24 : free(app(A,B),C)==(free(A,C)or free(B,C))                        [input]
  25 : free(abs(A),B)==free(A,s(B))                                     [input]
  26 : ~free(A,0) -> eta(abs(app(A,var(0))),subst(A,0,B))               [input]
  33 : lemmaE1(A,B,C)==(0=<C and eta(A,B)=>free(B,C)<=>free(A,C))       [input]
  34 : 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]
  35 : lemmaF3(A,B,C,D)                                                 [input]
  36 + 0=<i and~free(s,0)=>lemmaE1(abs(app(s,var(0))),subst(s,0,a),i),eta(s,t)and lemmaE1(s,t,k)=>lemmaE1(app(s,v),app(t,v),k)and lemmaE1(app(v,s),app(v,t),k),eta(s,t)and 0=<l and!A.(lemmaE1(s,t,A))=>lemmaE1(abs(s),abs(t),l) ->  [input]
  43 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0)       [expansion from 26]
  45 : 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 35 by [34]]
  46 : 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 45]
  48 : 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 46]
  49 + eta(s,t)and(0=<k and eta(s,t)=>free(t,k)<=>free(s,k))=>(0=<k and eta(app(s,v),app(t,v))=>free(t,k)or free(v,k)<=>free(s,k)or free(v,k))and(0=<k and eta(app(v,s),app(v,t))=>free(v,k)or free(t,k)<=>free(v,k)or free(s,k)),0=<i and~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>free(subst(s,0,a),i)<=>free(s,s(i))or 0=s(i),eta(s,t)and 0=<l and!A.(0=<A and eta(s,t)=>free(t,A)<=>free(s,A))=>0=<l and eta(abs(s),abs(t))=>free(t,s(l))<=>free(s,s(l)) ->  [reduction of 36 by [33,25,24,23,33,24,24,33,24,24,33,33,25,25,33]]
  50 + p$499,0=<i and~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>free(subst(s,0,a),i)<=>free(s,s(i))or 0=s(i),eta(s,t)and 0=<l and!A.(0=<A and eta(s,t)=>free(t,A)<=>free(s,A))=>0=<l and eta(abs(s),abs(t))=>free(t,s(l))<=>free(s,s(l)) ->  [expansion from 49]
  51 + p$499,eta(s,t)and(0=<k and eta(s,t)=>free(t,k)<=>free(s,k)) [expansion from 49]
  52 + (0=<k and eta(app(s,v),app(t,v))=>free(t,k)or free(v,k)<=>free(s,k)or free(v,k))and(0=<k and eta(app(v,s),app(v,t))=>free(v,k)or free(t,k)<=>free(v,k)or free(s,k)) -> p$499 [expansion from 49]
  53 + 0=<k and eta(app(s,v),app(t,v))=>free(t,k)or free(v,k)<=>free(s,k)or free(v,k),0=<k and eta(app(v,s),app(v,t))=>free(v,k)or free(t,k)<=>free(v,k)or free(s,k) -> p$499 [expansion from 52]
  54 + p$498,0=<i and~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>free(subst(s,0,a),i)<=>free(s,s(i))or 0=s(i),p$499 ->  [expansion from 50]
  55 + p$498,eta(s,t)and 0=<l and!A.(0=<A and eta(s,t)=>free(t,A)<=>free(s,A)) [expansion from 50]
  56 + 0=<l and eta(abs(s),abs(t))=>free(t,s(l))<=>free(s,s(l)) -> p$498 [expansion from 50]
  57 + p$497,p$499                                          [expansion from 51]
  58 + p$497 -> eta(s,t)                                    [expansion from 51]
  59 + p$497 -> 0=<k and eta(s,t)=>free(t,k)<=>free(s,k)    [expansion from 51]
  60 + p$497,0=<k,eta(s,t) -> free(t,k)==free(s,k)          [expansion from 59]
  61 + p$497,eta(s,t) -> k<0,free(t,k)==free(s,k) [totality resolution from 60]
  62 + p$496,0=<k and eta(app(s,v),app(t,v))=>free(t,k)or free(v,k)<=>free(s,k)or free(v,k) -> p$499 [expansion from 53]
  63 + p$496,0=<k and eta(app(v,s),app(v,t))                [expansion from 53]
  64 + (free(v,k)or free(t,k))==(free(v,k)or free(s,k)) -> p$496 [expansion from 53]
  65 + free(v,k)or free(t,k)=>free(v,k)or free(s,k),free(v,k)or free(s,k)=>free(v,k)or free(t,k) -> p$496 [expansion from 64]
  66 + p$495,p$498                                          [expansion from 55]
  67 + p$495 -> eta(s,t)and 0=<l                            [expansion from 55]
  68 + p$495 -> !A.(0=<A and eta(s,t)=>free(t,A)<=>free(s,A)) [expansion from 55]
  69 + p$495,0=<A,eta(s,t) -> free(t,A)==free(s,A)          [expansion from 68]
  70 + p$495,eta(s,t) -> A<0,free(t,A)==free(s,A) [totality resolution from 69]
  71 + p$494 -> p$498                                       [expansion from 56]
  72 + p$494,0=<l and eta(abs(s),abs(t))                    [expansion from 56]
  73 + free(t,s(l))==free(s,s(l)) -> p$494                  [expansion from 56]
  74 + free(t,s(l))=>free(s,s(l)),free(s,s(l))=>free(t,s(l)) -> p$494 [expansion from 73]
  75 + p$493,p$496 -> p$499                                 [expansion from 62]
  76 + p$493,0=<k and eta(app(s,v),app(t,v))                [expansion from 62]
  77 + (free(t,k)or free(v,k))==(free(s,k)or free(v,k)) -> p$493 [expansion from 62]
  78 + free(t,k)or free(v,k)=>free(s,k)or free(v,k),free(s,k)or free(v,k)=>free(t,k)or free(v,k) -> p$493 [expansion from 77]
  79 + p$492,p$496                                          [expansion from 63]
  80 + p$492 -> 0=<k                                        [expansion from 63]
  82 + p$491,free(v,k)or free(t,k)=>free(v,k)or free(s,k) -> p$496 [expansion from 65]
  83 + p$491,free(v,k)or free(s,k)                          [expansion from 65]
  84 + free(v,k)or free(t,k) -> p$491                       [expansion from 65]
  85 + p$491,free(v,k),free(s,k)                            [expansion from 83]
  86 + p$490,p$494                                          [expansion from 72]
  87 + p$490 -> 0=<l                                        [expansion from 72]
  89 + p$489,free(s,s(l))=>free(t,s(l)) -> p$494            [expansion from 74]
  90 + p$489,free(t,s(l))                                   [expansion from 74]
  91 + free(s,s(l)) -> p$489                                [expansion from 74]
  92 + p$488,p$493                                          [expansion from 76]
  93 + p$488 -> 0=<k                                        [expansion from 76]
  95 + p$487,free(t,k)or free(v,k)=>free(s,k)or free(v,k) -> p$493 [expansion from 78]
  96 + p$487,free(s,k)or free(v,k)                          [expansion from 78]
  97 + free(t,k)or free(v,k) -> p$487                       [expansion from 78]
  98 + p$487,free(s,k),free(v,k)                            [expansion from 96]
  99 + p$486,p$491 -> p$496                                 [expansion from 82]
 100 + p$486,free(v,k)or free(t,k)                          [expansion from 82]
 101 + free(v,k)or free(s,k) -> p$486                       [expansion from 82]
 102 + p$486,free(v,k),free(t,k)                           [expansion from 100]
 103 + p$485 -> p$491                                       [expansion from 84]
 104 + free(v,k) -> p$485                                   [expansion from 84]
 105 + free(t,k) -> p$485                                   [expansion from 84]
 106 + p$484,p$489 -> p$494                                 [expansion from 89]
 107 + p$484,free(s,s(l))                                   [expansion from 89]
 108 + free(t,s(l)) -> p$484                                [expansion from 89]
 109 + p$483,p$487 -> p$493                                 [expansion from 95]
 110 + p$483,free(t,k)or free(v,k)                          [expansion from 95]
 111 + free(s,k)or free(v,k) -> p$483                       [expansion from 95]
 112 + p$483,free(t,k),free(v,k)                           [expansion from 110]
 113 + p$482 -> p$487                                       [expansion from 97]
 114 + free(t,k) -> p$482                                   [expansion from 97]
 115 + free(v,k) -> p$482                                   [expansion from 97]
 116 + p$481 -> p$486                                      [expansion from 101]
 117 + free(v,k) -> p$481                                  [expansion from 101]
 118 + free(s,k) -> p$481                                  [expansion from 101]
 119 + p$480 -> p$483                                      [expansion from 111]
 120 + free(s,k) -> p$480                                  [expansion from 111]
 121 + free(v,k) -> p$480                                  [expansion from 111]
 122 + p$496,0=<k                             [negative chaining of 79 from 80]
 123 + p$494,0=<l                             [negative chaining of 86 from 87]
 124 + p$493,0=<k                             [negative chaining of 92 from 93]
 125 + p$499,eta(s,t)                         [negative chaining of 57 from 58]
 127 + p$498,eta(s,t)and 0=<l                 [negative chaining of 66 from 67]
 128 + p$479,p$498                                         [expansion from 127]
 129 + p$479 -> eta(s,t)                                   [expansion from 127]
 132 + p$498,eta(s,t)                       [negative chaining of 128 from 129]
 136 + p$491,free(s,k),p$485                 [negative chaining of 85 from 104]
 140 + p$491,free(s,k)                            [reduction of 136 by [103,L]]
 147 + p$487,free(s,k),p$482                 [negative chaining of 98 from 115]
 150 + p$487,free(s,k)                            [reduction of 147 by [113,L]]
 158 + p$497 -> p$499,k<0,free(t,k)==free(s,k) [negative chaining of 125 from 61]
 160 + free(t,k)==free(s,k),k<0,p$499                [reduction of 158 by [57]]
 161 + free(s,k) -> k<0,p$499,p$485         [negative chaining of 160 from 105]
 162 + free(s,k) -> k<0,p$499,p$482         [negative chaining of 160 from 114]
 163 + p$491,k<0,p$499,p$485                [negative chaining of 140 from 161]
 166 + p$491,k<0,p$499                            [reduction of 163 by [103,L]]
 168 + p$496,p$499,p$491                             [chaining of 122 from 166]
 169 + p$493,p$499,p$491                             [chaining of 124 from 166]
 170 + p$491,p$499                             [reduction of 169 by [75,168,L]]
 173 + p$486,free(t,k),p$481                [negative chaining of 102 from 117]
 177 + p$486,free(t,k)                            [reduction of 173 by [116,L]]
 182 + free(s,k),k<0,p$499,p$486                     [chaining of 160 from 177]
 183 + p$486,p$499,k<0                      [reduction of 182 by [118,116,L,L]]
 184 + p$496,p$499,p$486                             [chaining of 122 from 183]
 186 + p$496,p$499                             [reduction of 184 by [99,170,L]]
 190 + p$487,k<0,p$499,p$482                [negative chaining of 150 from 162]
 192 + p$499,p$487                 [reduction of 190 by [124,75,186,L,L,113,L]]
 197 + p$483,free(t,k),p$480                [negative chaining of 112 from 121]
 200 + p$483,free(t,k)                            [reduction of 197 by [119,L]]
 206 + free(s,k),k<0,p$499,p$483                     [chaining of 160 from 200]
 207 + p$499 [reduction of 206 by [120,119,L,L,124,75,186,L,L,109,75,186,L,192,L]]
 208 + 0=<i and~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>free(subst(s,0,a),i)<=>free(s,s(i))or 0=s(i),p$498 ->  [reduction of 54 by [207]]
 209 + p$495 -> p$498,free(t,A)==free(s,A),A<0 [negative chaining of 132 from 70]
 210 + A<0,free(t,A)==free(s,A),p$498                [reduction of 209 by [66]]
 213 + free(s,s(l)) -> p$498,s(l)<0,p$484   [negative chaining of 210 from 108]
 214 + free(s,s(l)),p$489,p$498,s(l)<0                [chaining of 90 from 210]
 217 + p$498,p$484                    [reduction of 213 by [107,11,123,71,L,L]]
 218 + p$489,p$498                   [reduction of 214 by [91,L,11,123,71,L,L]]
 221 + p$489 -> p$498,p$494                 [negative chaining of 217 from 106]
 222 + p$498                                   [reduction of 221 by [218,71,L]]
 223 + 0=<i and~free(s,0)=>0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>free(subst(s,0,a),i)<=>free(s,s(i))or 0=s(i) ->  [reduction of 208 by [222]]
 224 + 0=<i and~free(s,0)                                  [expansion from 223]
 225 + 0=<i and eta(abs(app(s,var(0))),subst(s,0,a))=>free(subst(s,0,a),i)<=>free(s,s(i))or 0=s(i) ->  [expansion from 223]
 226 + 0=<i                                                [expansion from 224]
 227 + ~free(s,0)                                          [expansion from 224]
 228 + free(s,0) ->                                        [expansion from 227]
 229 + 0=<i and eta(abs(app(s,var(0))),subst(s,0,a))       [expansion from 225]
 230 + free(subst(s,0,a),i)==(free(s,s(i))or 0=s(i)) ->    [expansion from 225]
 231 + 0=<i                                  [reduction of 229 by [43,228,L,L]]
 232 + (i<0 and free(s,i)or free(s,s(i)))==(free(s,s(i))or 0=s(i)) ->  [reduction of 230 by [48,226,L,231,L,228,L,L]]
 233 + i<0 and free(s,i)or free(s,s(i))=>free(s,s(i))or 0=s(i),free(s,s(i))or 0=s(i)=>i<0 and free(s,i)or free(s,s(i)) ->  [expansion from 232]
 234 + p$478,i<0 and free(s,i)or free(s,s(i))=>free(s,s(i))or 0=s(i) ->  [expansion from 233]
 235 + p$478,free(s,s(i))or 0=s(i)                         [expansion from 233]
 236 + i<0 and free(s,i)or free(s,s(i)) -> p$478           [expansion from 233]
 237 + p$478,free(s,s(i)),0=s(i)                           [expansion from 235]
 238 + p$477,p$478 ->                                      [expansion from 234]
 239 + p$477,i<0 and free(s,i)or free(s,s(i))              [expansion from 234]
 240 + free(s,s(i))or 0=s(i) -> p$477                      [expansion from 234]
 241 + p$477,i<0 and free(s,i),free(s,s(i))                [expansion from 239]
 242 + p$476 -> p$478                                      [expansion from 236]
 244 + free(s,s(i)) -> p$476                               [expansion from 236]
 247 + p$475 -> p$477                                      [expansion from 240]
 248 + free(s,s(i)) -> p$475                               [expansion from 240]
 250 + p$478,s(i)=0,p$476                   [negative chaining of 237 from 244]
 252 + p$478,s(i)=0                               [reduction of 250 by [242,L]]
 253 + i<0,p$478                                      [chaining of 11 from 252]
 262 + p$478                                      [reduction of 253 by [226,L]]
 264 + p$477 ->                                     [reduction of 238 by [262]]
 265 + free(s,s(i)),i<0 and free(s,i)             [reduction of 241 by [264,L]]
 266 + p$475 ->                                   [reduction of 247 by [264,L]]
 268 + free(s,s(i)) ->                            [reduction of 248 by [266,L]]
 269 + i<0 and free(s,i)                          [reduction of 265 by [268,L]]
 270 + i<0                                                 [expansion from 269]
 272 + false                                      [reduction of 270 by [226,L]]

Length = 159, Depth = 37



Total time: 17000 milliseconds

Number of forward inferences: 85
Number of tableau inferences: 83
Number of kept clauses: 179

*/