use(subst).
use(int).
use(etas).
use(lemmaE6).
use(lemmaE7).
use(lemmaE3b).


lemmaE6(S,T,I).

etas(S,T) -> etas(abs(S),abs(T)). %noetig
lemmaE3b(S,T,U,V).

%Induktionsanfang der Induktion ueber die Lambda-Terme

(0=<k => lemmaE7(s,t,var(k),i)),

%2 Induktionsschritte

(all(I,all(S,all(T,lemmaE7(S,T,u,I)))) => lemmaE7(s,t,abs(u),i)),

((lemmaE7(s,t,u,i) and lemmaE7(s,t,v,i)) => lemmaE7(s,t,app(u,v),i)) -> [].


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

top_predicates_precedence([lemmaE6,lemmaE7,lemmaE3b]).

/*
Proof:
======

  14 : A<B -> subst(var(B),A,C)=var(p(B))                               [input]
  15 : subst(var(A),A,B)=B                                              [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]
  43 : etas(A,A)                                                        [input]
  44 : eta(A,B) -> etas(A,B)                                            [input]
  45 : etas(A,B)and eta(B,C) -> etas(A,C)                               [input]
  46 : lemmaE6(A,B,C)==(0=<C and eta(A,B)=>eta(lift(A,C),lift(B,C)))    [input]
  47 : lemmaE7(A,B,C,D)==(0=<D and eta(A,B)=>etas(subst(C,D,A),subst(C,D,B))) [input]
  48 : lemmaE3b(A,B,C,D)==(etas(A,B)=>etas(C,D)=>etas(app(A,C),app(B,D))) [input]
  49 : lemmaE6(A,B,C)                                                   [input]
  50 : etas(A,B) -> etas(abs(A),abs(B))                                 [input]
  51 : lemmaE3b(A,B,C,D)                                                [input]
  52 : 0=<k=>lemmaE7(s,t,var(k),i),!A,B,C.(lemmaE7(B,C,u,A))=>lemmaE7(s,t,abs(u),i),lemmaE7(s,t,u,i)and lemmaE7(s,t,v,i)=>lemmaE7(s,t,app(u,v),i) ->  [input]
  55 : A=<B,subst(var(A),B,C)=var(p(A))           [totality resolution from 14]
  56 : A=<B,subst(var(B),A,C)=var(B)              [totality resolution from 16]
  64 : etas(A,B),eta(B,C) -> etas(A,C)                      [expansion from 45]
  65 : 0=<A and eta(B,C)=>eta(lift(B,A),lift(C,A))    [reduction of 49 by [46]]
  66 : 0=<A,eta(B,C) -> eta(lift(B,A),lift(C,A))            [expansion from 65]
  67 : eta(A,B) -> C<0,eta(lift(A,C),lift(B,C))   [totality resolution from 66]
  68 : etas(A,B)=>etas(C,D)=>etas(app(A,C),app(B,D))  [reduction of 51 by [48]]
  69 : etas(A,B),etas(C,D) -> etas(app(A,C),app(B,D))       [expansion from 68]
  70 : !A,B,C.(0=<A and eta(B,C)=>etas(subst(u,A,B),subst(u,A,C)))=>0=<i and eta(s,t)=>etas(abs(subst(u,s(i),lift(s,0))),abs(subst(u,s(i),lift(t,0)))),0=<k=>0=<i and eta(s,t)=>etas(subst(var(k),i,s),subst(var(k),i,t)),(0=<i and eta(s,t)=>etas(subst(u,i,s),subst(u,i,t)))and(0=<i and eta(s,t)=>etas(subst(v,i,s),subst(v,i,t)))=>0=<i and eta(s,t)=>etas(app(subst(u,i,s),subst(v,i,s)),app(subst(u,i,t),subst(v,i,t))) ->  [reduction of 52 by [47,47,18,18,47,47,17,17,47,47]]
  71 : p$199,0=<k=>0=<i and eta(s,t)=>etas(subst(var(k),i,s),subst(var(k),i,t)),!A,B,C.(0=<A and eta(B,C)=>etas(subst(u,A,B),subst(u,A,C)))=>0=<i and eta(s,t)=>etas(abs(subst(u,s(i),lift(s,0))),abs(subst(u,s(i),lift(t,0)))) ->  [expansion from 70]
  72 : p$199,(0=<i and eta(s,t)=>etas(subst(u,i,s),subst(u,i,t)))and(0=<i and eta(s,t)=>etas(subst(v,i,s),subst(v,i,t))) [expansion from 70]
  73 : 0=<i and eta(s,t)=>etas(app(subst(u,i,s),subst(v,i,s)),app(subst(u,i,t),subst(v,i,t))) -> p$199 [expansion from 70]
  74 : p$198,0=<k=>0=<i and eta(s,t)=>etas(subst(var(k),i,s),subst(var(k),i,t)),p$199 ->  [expansion from 71]
  75 : p$198,!A,B,C.(0=<A and eta(B,C)=>etas(subst(u,A,B),subst(u,A,C))) [expansion from 71]
  76 : 0=<i and eta(s,t)=>etas(abs(subst(u,s(i),lift(s,0))),abs(subst(u,s(i),lift(t,0)))) -> p$198 [expansion from 71]
  77 : 0=<A,eta(B,C) -> p$198,etas(subst(u,A,B),subst(u,A,C)) [expansion from 75]
  78 : eta(A,B) -> C<0,p$198,etas(subst(u,C,A),subst(u,C,B)) [totality resolution from 77]
  79 : p$197,p$199                                          [expansion from 72]
  80 : p$197 -> 0=<i and eta(s,t)=>etas(subst(u,i,s),subst(u,i,t)) [expansion from 72]
  81 : p$197 -> 0=<i and eta(s,t)=>etas(subst(v,i,s),subst(v,i,t)) [expansion from 72]
  82 : p$197,0=<i,eta(s,t) -> etas(subst(u,i,s),subst(u,i,t)) [expansion from 80]
  83 : p$197,eta(s,t) -> i<0,etas(subst(u,i,s),subst(u,i,t)) [totality resolution from 82]
  84 : p$197,0=<i,eta(s,t) -> etas(subst(v,i,s),subst(v,i,t)) [expansion from 81]
  85 : p$197,eta(s,t) -> i<0,etas(subst(v,i,s),subst(v,i,t)) [totality resolution from 84]
  86 : p$196 -> p$199                                       [expansion from 73]
  87 : p$196,0=<i and eta(s,t)                              [expansion from 73]
  88 : etas(app(subst(u,i,s),subst(v,i,s)),app(subst(u,i,t),subst(v,i,t))) -> p$196 [expansion from 73]
  89 : p$195 -> p$198                                       [expansion from 76]
  90 : p$195,0=<i and eta(s,t)                              [expansion from 76]
  91 : etas(abs(subst(u,s(i),lift(s,0))),abs(subst(u,s(i),lift(t,0)))) -> p$195 [expansion from 76]
  92 : p$194,p$196                                          [expansion from 87]
  93 : p$194 -> 0=<i                                        [expansion from 87]
  94 : p$194 -> eta(s,t)                                    [expansion from 87]
  95 : p$194,p$195                                          [expansion from 90]
  96 : p$196,0=<i                             [negative chaining of 92 from 93]
  97 : p$195,0=<i                             [negative chaining of 95 from 93]
  98 : p$196,eta(s,t)                         [negative chaining of 92 from 94]
  99 : p$195,eta(s,t)                         [negative chaining of 95 from 94]
 101 : etas(A,s) -> p$195,etas(A,t)           [negative chaining of 99 from 64]
 103 : etas(subst(u,i,s),subst(u,i,t)),etas(subst(v,i,s),subst(v,i,t)) -> p$196 [negative chaining of 69 from 88]
 107 : etas(subst(u,s(i),lift(s,0)),subst(u,s(i),lift(t,0))) -> p$195 [negative chaining of 50 from 91]
 110 : p$197 -> p$196,etas(subst(u,i,s),subst(u,i,t)),i<0 [negative chaining of 98 from 83]
 112 : p$197 -> p$196,etas(subst(u,i,s),subst(u,i,t)) [reduction of 110 by [96,L]]
 114 : p$199,etas(subst(u,i,s),subst(u,i,t)),p$196 [negative chaining of 79 from 112]
 115 : p$199,etas(subst(u,i,s),subst(u,i,t))       [reduction of 114 by [86,L]]
 119 : p$197 -> p$196,etas(subst(v,i,s),subst(v,i,t)),i<0 [negative chaining of 98 from 85]
 121 : p$197 -> p$196,etas(subst(v,i,s),subst(v,i,t)) [reduction of 119 by [96,L]]
 123 : p$199,etas(subst(v,i,s),subst(v,i,t)),p$196 [negative chaining of 79 from 121]
 124 : p$199                             [reduction of 123 by [103,115,L,86,L]]
 125 : 0=<k=>0=<i and eta(s,t)=>etas(subst(var(k),i,s),subst(var(k),i,t)),p$198 ->  [reduction of 74 by [124]]
 126 : p$193,p$198 ->                                      [expansion from 125]
 128 : 0=<i and eta(s,t)=>etas(subst(var(k),i,s),subst(var(k),i,t)) -> p$193 [expansion from 125]
 129 : p$192 -> p$193                                      [expansion from 128]
 130 : p$192,0=<i and eta(s,t)                             [expansion from 128]
 131 : etas(subst(var(k),i,s),subst(var(k),i,t)) -> p$192  [expansion from 128]
 132 : p$194,p$192                                         [expansion from 130]
 134 : etas(subst(var(k),i,s),var(k)) -> i=<k,p$192 [negative chaining of 56 from 131]
 136 : etas(subst(var(k),i,s),var(p(k))) -> k=<i,p$192 [negative chaining of 55 from 131]
 138 : p$192,i=<k                                 [reduction of 134 by [56,43]]
 139 : p$192,k=i                              [reduction of 136 by [55,43,138]]
 141 : etas(subst(var(k),i,s),subst(var(i),i,t)) -> p$192,p$192 [negative chaining of 139 from 131]
 143 : etas(subst(var(k),i,s),subst(var(i),i,t)) -> p$192 [condensement of 141]
 144 : etas(s,t) -> p$192                     [reduction of 143 by [15,139,15]]
 146 : eta(s,t) -> p$192                     [negative chaining of 44 from 144]
 148 : etas(s,s) -> p$195,p$192             [negative chaining of 101 from 144]
 150 : p$192,p$195                                   [reduction of 148 by [43]]
 152 : p$195,p$193                          [negative chaining of 150 from 129]
 154 : p$198 -> p$195                       [negative chaining of 152 from 126]
 156 : eta(lift(s,0),lift(t,0)) -> p$198,s(i)<0,p$195 [negative chaining of 78 from 107]
 158 : p$195                        [reduction of 156 by [67,99,154,L,36,97,L]]
 159 : p$198                                         [reduction of 89 by [158]]
 160 : p$193 ->                                     [reduction of 126 by [159]]
 163 : p$192 ->                                   [reduction of 129 by [160,L]]
 164 : p$194                                      [reduction of 132 by [163,L]]
 170 : eta(s,t) ->                                [reduction of 146 by [163,L]]
 172 : false                                   [reduction of 94 by [164,170,L]]

Length = 92, Depth = 30



Total time: 25820 milliseconds

Number of forward inferences: 39
Number of tableau inferences: 26
Number of kept clauses: 120

*/