use(subst).
use(int).
use(pbeta).
use(lemmaP1).
use(subst_lemmas).

lemma2(T,S,J,I).

% Proof by induction over pbeta:

(0=<i => lemmaP1(var(i),var(i),j)),

((pbeta(s,t) and lemmaP1(s,t,j) and pbeta(u,v) and lemmaP1(u,v,j))
  => lemmaP1(app(s,u),app(t,v),j)),

(all(J,pbeta(s,t) and lemmaP1(s,t,J)) => lemmaP1(abs(s),abs(t),j)),

((all(J,(pbeta(s,t) and lemmaP1(s,t,J) and
  pbeta(u,v) and lemmaP1(u,v,J)))) =>
  lemmaP1(app(abs(s),u),subst(t,0,v),j)) -> [].

option([var_overlaps(off),search_depth(1)]).


/*
Proof:
======

  11 : A<s(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]
  40 : pbeta(A,B) -> pbeta(abs(A),abs(B))                               [input]
  41 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(A,C),app(B,D))               [input]
  42 : pbeta(A,B) -> pbeta(C,D)=>pbeta(app(abs(A),C),subst(B,0,D))      [input]
  43 : pbeta(A,A)                                                       [input]
  44 : lemmaP1(A,B,C)==(0=<C and pbeta(A,B)=>pbeta(lift(A,C),lift(B,C))) [input]
  46 : 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]
  52 : lemma2(A,B,C,D)                                                  [input]
  53 : 0=<i=>lemmaP1(var(i),var(i),j),pbeta(s,t)and lemmaP1(s,t,j)and pbeta(u,v)and lemmaP1(u,v,j)=>lemmaP1(app(s,u),app(t,v),j),!A.(pbeta(s,t)and lemmaP1(s,t,A))=>lemmaP1(abs(s),abs(t),j),!B.(pbeta(s,t)and lemmaP1(s,t,B)and pbeta(u,v)and lemmaP1(u,v,B))=>lemmaP1(app(abs(s),u),subst(t,0,v),j) ->  [input]
  65 : pbeta(A,B),pbeta(C,D) -> pbeta(app(A,C),app(B,D))    [expansion from 41]
  66 : pbeta(A,B),pbeta(C,D) -> pbeta(app(abs(A),C),subst(B,0,D)) [expansion from 42]
  67 : A<s(B)and 0=<A=>lift(subst(C,A,D),B)=subst(lift(C,s(B)),A,lift(D,B)) [reduction of 52 by [46]]
  68 : A<s(B),0=<A -> lift(subst(C,A,D),B)=subst(lift(C,s(B)),A,lift(D,B)) [expansion from 67]
  70 : A<0,s(B)=<A,lift(subst(C,A,D),B)=subst(lift(C,s(B)),A,lift(D,B)) [totality resolution from 68]
  71 : !A.(pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A))))=>0=<j and pbeta(abs(s),abs(t))=>pbeta(abs(lift(s,s(j))),abs(lift(t,s(j)))),pbeta(s,t)and(0=<j and pbeta(s,t)=>pbeta(lift(s,j),lift(t,j)))and pbeta(u,v)and(0=<j and pbeta(u,v)=>pbeta(lift(u,j),lift(v,j)))=>0=<j and pbeta(app(s,u),app(t,v))=>pbeta(app(lift(s,j),lift(u,j)),app(lift(t,j),lift(v,j))),!B.(pbeta(s,t)and(0=<B and pbeta(s,t)=>pbeta(lift(s,B),lift(t,B)))and pbeta(u,v)and(0=<B and pbeta(u,v)=>pbeta(lift(u,B),lift(v,B))))=>0=<j and pbeta(app(abs(s),u),subst(t,0,v))=>pbeta(app(abs(lift(s,s(j))),lift(u,j)),lift(subst(t,0,v),j)) ->  [reduction of 53 by [44,43,43,L,L,L,44,21,21,44,44,44,22,22,44,44,21,22,44,44]]
  72 : p$499,pbeta(s,t)and(0=<j and pbeta(s,t)=>pbeta(lift(s,j),lift(t,j)))and pbeta(u,v)and(0=<j and pbeta(u,v)=>pbeta(lift(u,j),lift(v,j)))=>0=<j and pbeta(app(s,u),app(t,v))=>pbeta(app(lift(s,j),lift(u,j)),app(lift(t,j),lift(v,j))),!A.(pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A)))and pbeta(u,v)and(0=<A and pbeta(u,v)=>pbeta(lift(u,A),lift(v,A))))=>0=<j and pbeta(app(abs(s),u),subst(t,0,v))=>pbeta(app(abs(lift(s,s(j))),lift(u,j)),lift(subst(t,0,v),j)) ->  [expansion from 71]
  73 : p$499,!A.(pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A)))) [expansion from 71]
  74 : 0=<j and pbeta(abs(s),abs(t))=>pbeta(abs(lift(s,s(j))),abs(lift(t,s(j)))) -> p$499 [expansion from 71]
  75 : p$499,pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A))) [expansion from 73]
  76 : p$498,pbeta(s,t)and(0=<j and pbeta(s,t)=>pbeta(lift(s,j),lift(t,j)))and pbeta(u,v)and(0=<j and pbeta(u,v)=>pbeta(lift(u,j),lift(v,j)))=>0=<j and pbeta(app(s,u),app(t,v))=>pbeta(app(lift(s,j),lift(u,j)),app(lift(t,j),lift(v,j))),p$499 ->  [expansion from 72]
  77 : p$498,!A.(pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A)))and pbeta(u,v)and(0=<A and pbeta(u,v)=>pbeta(lift(u,A),lift(v,A)))) [expansion from 72]
  78 : 0=<j and pbeta(app(abs(s),u),subst(t,0,v))=>pbeta(app(abs(lift(s,s(j))),lift(u,j)),lift(subst(t,0,v),j)) -> p$498 [expansion from 72]
  79 : p$498,pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A)))and pbeta(u,v)and(0=<A and pbeta(u,v)=>pbeta(lift(u,A),lift(v,A))) [expansion from 77]
  80 : p$497(A),p$499                                       [expansion from 75]
  81 : p$497(A) -> pbeta(s,t)                               [expansion from 75]
  82 : p$497(A) -> 0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A)) [expansion from 75]
  83 : p$497(A),0=<A,pbeta(s,t) -> pbeta(lift(s,A),lift(t,A)) [expansion from 82]
  84 : p$497(A),pbeta(s,t) -> A<0,pbeta(lift(s,A),lift(t,A)) [totality resolution from 83]
  85 : p$497(A) -> pbeta(lift(s,A),lift(t,A)),A<0     [reduction of 84 by [81]]
  86 : p$496 -> p$499                                       [expansion from 74]
  87 : p$496,0=<j and pbeta(abs(s),abs(t))                  [expansion from 74]
  88 : pbeta(abs(lift(s,s(j))),abs(lift(t,s(j)))) -> p$496  [expansion from 74]
  89 : p$495,p$498,p$499 ->                                 [expansion from 76]
  90 : p$495,pbeta(s,t)and(0=<j and pbeta(s,t)=>pbeta(lift(s,j),lift(t,j)))and pbeta(u,v)and(0=<j and pbeta(u,v)=>pbeta(lift(u,j),lift(v,j))) [expansion from 76]
  91 : 0=<j and pbeta(app(s,u),app(t,v))=>pbeta(app(lift(s,j),lift(u,j)),app(lift(t,j),lift(v,j))) -> p$495 [expansion from 76]
  92 : p$494(A),p$498                                       [expansion from 79]
  93 : p$494(A) -> pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A)))and pbeta(u,v) [expansion from 79]
  94 : p$494(A) -> 0=<A and pbeta(u,v)=>pbeta(lift(u,A),lift(v,A)) [expansion from 79]
  95 : p$494(A),0=<A,pbeta(u,v) -> pbeta(lift(u,A),lift(v,A)) [expansion from 94]
  96 : p$494(A),pbeta(u,v) -> A<0,pbeta(lift(u,A),lift(v,A)) [totality resolution from 95]
  97 : p$493 -> p$498                                       [expansion from 78]
  98 : p$493,0=<j and pbeta(app(abs(s),u),subst(t,0,v))     [expansion from 78]
  99 : pbeta(app(abs(lift(s,s(j))),lift(u,j)),lift(subst(t,0,v),j)) -> p$493 [expansion from 78]
 100 : p$492,p$496                                          [expansion from 87]
 101 : p$492 -> 0=<j                                        [expansion from 87]
 103 : p$494(j),p$495                                       [expansion from 90]
 104 : p$491 -> p$495                                       [expansion from 91]
 105 : p$491,0=<j and pbeta(app(s,u),app(t,v))              [expansion from 91]
 106 : pbeta(app(lift(s,j),lift(u,j)),app(lift(t,j),lift(v,j))) -> p$491 [expansion from 91]
 107 : p$494(A) -> p$490(A)                                 [expansion from 93]
 108 : p$490(A) -> pbeta(s,t)and(0=<A and pbeta(s,t)=>pbeta(lift(s,A),lift(t,A))) [expansion from 93]
 109 : p$490(A) -> pbeta(u,v)                               [expansion from 93]
 110 : p$489,p$493                                          [expansion from 98]
 111 : p$489 -> 0=<j                                        [expansion from 98]
 113 : p$488,p$491                                         [expansion from 105]
 114 : p$488 -> 0=<j                                       [expansion from 105]
 116 : p$490(A) -> p$497(A)                                [expansion from 108]
 123 : p$496,0=<j                           [negative chaining of 100 from 101]
 124 : p$493,0=<j                           [negative chaining of 110 from 111]
 125 : p$491,0=<j                           [negative chaining of 113 from 114]
 126 : p$494(A) -> p$497(A)                 [negative chaining of 107 from 116]
 131 : p$495,p$497(j)                       [negative chaining of 103 from 126]
 134 : p$494(A) -> pbeta(u,v)               [negative chaining of 107 from 109]
 135 : p$495,pbeta(u,v)                     [negative chaining of 103 from 134]
 141 : pbeta(lift(s,s(j)),lift(t,s(j))) -> p$496 [negative chaining of 40 from 88]
 142 : p$497(s(j)) -> s(j)<0,p$496           [negative chaining of 85 from 141]
 143 : p$497(s(j)) -> p$496                    [reduction of 142 by [36,123,L]]
 144 : p$499,p$496                           [negative chaining of 80 from 143]
 145 : p$499                                       [reduction of 144 by [86,L]]
 146 : p$495,p$498 ->                                [reduction of 89 by [145]]
 147 : pbeta(lift(s,j),lift(t,j)),pbeta(lift(u,j),lift(v,j)) -> p$491 [negative chaining of 65 from 106]
 153 : p$494(A) -> p$495,pbeta(lift(u,A),lift(v,A)),A<0 [negative chaining of 135 from 96]
 154 : p$494(j),pbeta(lift(s,j),lift(t,j)) -> p$495,j<0,p$491 [negative chaining of 153 from 147]
 155 : p$495                     [reduction of 154 by [103,85,131,125,L,104,L]]
 156 : p$498 ->                                     [reduction of 146 by [155]]
 157 : p$493 ->                                    [reduction of 97 by [156,L]]
 158 : p$494(A)                                    [reduction of 92 by [156,L]]
 159 : pbeta(app(abs(lift(s,s(j))),lift(u,j)),lift(subst(t,0,v),j)) ->  [reduction of 99 by [157,L]]
 161 : 0=<j                                       [reduction of 124 by [157,L]]
 163 : p$497(A)                                     [reduction of 126 by [158]]
 164 : pbeta(u,v)                                   [reduction of 134 by [158]]
 166 : A<0,pbeta(lift(u,A),lift(v,A))            [reduction of 96 by [164,158]]
 168 : A<0,pbeta(lift(s,A),lift(t,A))                [reduction of 85 by [163]]
 181 : pbeta(A,lift(B,s(C))),pbeta(D,lift(E,C)) -> pbeta(app(abs(A),D),lift(subst(B,0,E),C)),s(C)=<0 [chaining of 70 from 66]
 185 : pbeta(lift(s,s(j)),lift(t,s(j))),pbeta(lift(u,j),lift(v,j)) -> s(j)=<0 [negative chaining of 181 from 159]
 186 : s(j)=0                      [reduction of 185 by [168,166,161,L,36,161]]
 189 : j<0                                            [chaining of 11 from 186]
 197 : false                                      [reduction of 189 by [161,L]]

Length = 91, Depth = 20



Total time: 9680 milliseconds

Number of forward inferences: 55
Number of tableau inferences: 38
Number of kept clauses: 139
*/