use(subst).
use(int).
use(beta).
use(lemmaB2).
use(subst_lemmas).

lemma5(T,U,V,I,J).

%Induktionsanfang der Induktion ueber beta

lemmaB2(app(abs(s),t),subst(s,0,t),u,i),

%2 Induktionsschritte

((lemmaB2(s,t,w,i) and beta(s,t)) =>
 (lemmaB2(app(s,u),app(t,u),w,i) and lemmaB2(app(u,s),app(u,t),w,i))),

((all(I,all(U,lemmaB2(s,t,U,I))) and beta(s,t)) =>
  lemmaB2(abs(s),abs(t),u,i)) -> [].

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


/*
Proof:
======

  11 : A<s(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 : beta(app(abs(A),B),subst(A,0,B))                                 [input]
  40 : beta(A,B) -> beta(app(C,A),app(C,B))                             [input]
  41 : beta(A,B) -> beta(app(A,C),app(B,C))                             [input]
  42 : beta(A,B) -> beta(abs(A),abs(B))                                 [input]
  46 : lemmaB2(A,B,C,D)==(0=<D=>beta(A,B)=>beta(subst(A,D,C),subst(B,D,C))) [input]
  51 : 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]
  54 : lemma5(A,B,C,D,E)                                                [input]
  55 : lemmaB2(app(abs(s),t),subst(s,0,t),u,i),lemmaB2(s,t,w,i)and beta(s,t)=>lemmaB2(app(s,u),app(t,u),w,i)and lemmaB2(app(u,s),app(u,t),w,i),!A,B.(lemmaB2(s,t,B,A)) and beta(s,t)=>lemmaB2(abs(s),abs(t),u,i) ->  [input]
  67 : 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 54 by [51]]
  68 : 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 67]
  70 : 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 68]
  71 : (0=<i=>beta(s,t)=>beta(subst(s,i,w),subst(t,i,w)))and beta(s,t)=>(0=<i=>beta(app(s,u),app(t,u))=>beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))))and(0=<i=>beta(app(u,s),app(u,t))=>beta(app(subst(u,i,w),subst(s,i,w)),app(subst(u,i,w),subst(t,i,w)))),0=<i=>beta(app(abs(subst(s,s(i),lift(u,0))),subst(t,i,u)),subst(subst(s,0,t),i,u)),!A,B.(0=<A=>beta(s,t)=>beta(subst(s,A,B),subst(t,A,B))) and beta(s,t)=>0=<i=>beta(abs(s),abs(t))=>beta(abs(subst(s,s(i),lift(u,0))),abs(subst(t,s(i),lift(u,0)))) ->  [reduction of 55 by [46,17,18,39,L,46,17,17,46,17,17,46,46,18,18,46]]
  72 : p$199,0=<i=>beta(app(abs(subst(s,s(i),lift(u,0))),subst(t,i,u)),subst(subst(s,0,t),i,u)),(0=<i=>beta(s,t)=>beta(subst(s,i,w),subst(t,i,w)))and beta(s,t)=>(0=<i=>beta(app(s,u),app(t,u))=>beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))))and(0=<i=>beta(app(u,s),app(u,t))=>beta(app(subst(u,i,w),subst(s,i,w)),app(subst(u,i,w),subst(t,i,w)))) ->  [expansion from 71]
  73 : p$199,!A,B.(0=<A=>beta(s,t)=>beta(subst(s,A,B),subst(t,A,B))) and beta(s,t) [expansion from 71]
  74 : 0=<i=>beta(abs(s),abs(t))=>beta(abs(subst(s,s(i),lift(u,0))),abs(subst(t,s(i),lift(u,0)))) -> p$199 [expansion from 71]
  75 : p$198,0=<i=>beta(app(abs(subst(s,s(i),lift(u,0))),subst(t,i,u)),subst(subst(s,0,t),i,u)),p$199 ->  [expansion from 72]
  76 : p$198,(0=<i=>beta(s,t)=>beta(subst(s,i,w),subst(t,i,w)))and beta(s,t) [expansion from 72]
  77 : (0=<i=>beta(app(s,u),app(t,u))=>beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))))and(0=<i=>beta(app(u,s),app(u,t))=>beta(app(subst(u,i,w),subst(s,i,w)),app(subst(u,i,w),subst(t,i,w)))) -> p$198 [expansion from 72]
  78 : 0=<i=>beta(app(s,u),app(t,u))=>beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))),0=<i=>beta(app(u,s),app(u,t))=>beta(app(subst(u,i,w),subst(s,i,w)),app(subst(u,i,w),subst(t,i,w))) -> p$198 [expansion from 77]
  79 : p$197,p$199                                          [expansion from 73]
  80 : p$197 -> !A,B.(0=<A=>beta(s,t)=>beta(subst(s,A,B),subst(t,A,B))) [expansion from 73]
  81 : p$197 -> beta(s,t)                                   [expansion from 73]
  82 : p$197,0=<A,beta(s,t) -> beta(subst(s,A,B),subst(t,A,B)) [expansion from 80]
  83 : p$197,beta(s,t) -> A<0,beta(subst(s,A,B),subst(t,A,B)) [totality resolution from 82]
  84 : p$196 -> p$199                                       [expansion from 74]
  85 : p$196,0=<i                                           [expansion from 74]
  86 : beta(abs(s),abs(t))=>beta(abs(subst(s,s(i),lift(u,0))),abs(subst(t,s(i),lift(u,0)))) -> p$196 [expansion from 74]
  87 : p$195,p$198                                          [expansion from 76]
  88 : p$195 -> 0=<i=>beta(s,t)=>beta(subst(s,i,w),subst(t,i,w)) [expansion from 76]
  89 : p$195 -> beta(s,t)                                   [expansion from 76]
  90 : p$195,0=<i,beta(s,t) -> beta(subst(s,i,w),subst(t,i,w)) [expansion from 88]
  91 : p$195,beta(s,t) -> i<0,beta(subst(s,i,w),subst(t,i,w)) [totality resolution from 90]
  92 : p$194,0=<i=>beta(app(s,u),app(t,u))=>beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))) -> p$198 [expansion from 78]
  93 : p$194,0=<i                                           [expansion from 78]
  94 : beta(app(u,s),app(u,t))=>beta(app(subst(u,i,w),subst(s,i,w)),app(subst(u,i,w),subst(t,i,w))) -> p$194 [expansion from 78]
  95 : p$193 -> p$196                                       [expansion from 86]
  97 : beta(abs(subst(s,s(i),lift(u,0))),abs(subst(t,s(i),lift(u,0)))) -> p$193 [expansion from 86]
  98 : p$192,p$194 -> p$198                                 [expansion from 92]
  99 : p$192,0=<i                                           [expansion from 92]
 100 : beta(app(s,u),app(t,u))=>beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))) -> p$192 [expansion from 92]
 101 : p$191 -> p$194                                       [expansion from 94]
 103 : beta(app(subst(u,i,w),subst(s,i,w)),app(subst(u,i,w),subst(t,i,w))) -> p$191 [expansion from 94]
 104 : p$190 -> p$192                                      [expansion from 100]
 106 : beta(app(subst(s,i,w),subst(u,i,w)),app(subst(t,i,w),subst(u,i,w))) -> p$190 [expansion from 100]
 113 : p$199,beta(s,t)                        [negative chaining of 79 from 81]
 114 : p$198,beta(s,t)                        [negative chaining of 87 from 89]
 135 : beta(subst(s,i,w),subst(t,i,w)) -> p$191 [negative chaining of 40 from 103]
 136 : beta(subst(s,i,w),subst(t,i,w)) -> p$190 [negative chaining of 41 from 106]
 137 : beta(subst(s,s(i),lift(u,0)),subst(t,s(i),lift(u,0))) -> p$193 [negative chaining of 42 from 97]
 138 : p$197 -> p$199,beta(subst(s,A,B),subst(t,A,B)),A<0 [negative chaining of 113 from 83]
 140 : A<0,beta(subst(s,A,B),subst(t,A,B)),p$199     [reduction of 138 by [79]]
 143 : p$199,s(i)<0,p$193                   [negative chaining of 140 from 137]
 146 : p$199                     [reduction of 143 by [36,85,84,L,L,95,84,L,L]]
 147 : 0=<i=>beta(app(abs(subst(s,s(i),lift(u,0))),subst(t,i,u)),subst(subst(s,0,t),i,u)),p$198 ->  [reduction of 75 by [146]]
 148 : p$195 -> p$198,beta(subst(s,i,w),subst(t,i,w)),i<0 [negative chaining of 114 from 91]
 149 : i<0,beta(subst(s,i,w),subst(t,i,w)),p$198     [reduction of 148 by [87]]
 151 : p$198,i<0,p$191                      [negative chaining of 149 from 135]
 152 : p$198,i<0,p$190                      [negative chaining of 149 from 136]
 154 : p$194,p$198,p$191                              [chaining of 93 from 151]
 156 : p$194,p$198                                [reduction of 154 by [101,L]]
 161 : p$192,p$198,p$190                              [chaining of 99 from 152]
 163 : p$198                    [reduction of 161 by [98,156,L,104,98,156,L,L]]
 164 : 0=<i=>beta(app(abs(subst(s,s(i),lift(u,0))),subst(t,i,u)),subst(subst(s,0,t),i,u)) ->  [reduction of 147 by [163]]
 165 : 0=<i                                                [expansion from 164]
 166 : beta(app(abs(subst(s,s(i),lift(u,0))),subst(t,i,u)),subst(subst(s,0,t),i,u)) ->  [expansion from 164]
 181 : beta(app(abs(subst(A,s(B),lift(C,0))),subst(D,B,C)),subst(subst(A,0,D),B,C)),s(B)=<0 {[conj([subst(subst(A,s(B),lift(C,0)),0,subst(D,B,C))>subst(subst(A,0,D),B,C)],[],[])]} [chaining of 70 from 39]
 203 : s(i)=<0                              [negative chaining of 181 from 166]
 204 : s(i)=0                                    [reduction of 203 by [36,165]]
 208 : i<0                                            [chaining of 11 from 204]
 217 : false                                      [reduction of 208 by [165,L]]

Length = 74, Depth = 19



Total time: 42280 milliseconds

Number of forward inferences: 86
Number of tableau inferences: 32
Number of kept clauses: 140
*/