use(subst).
use(int_lemmas).
use(subst_lemmas).



% use Lemma 1
lemma1(T,I,K).

% induction proof for lemma2(T,S,I,K)

goal
lemma2(var(j),s,i,k),
(all(J,all(I,all(S,lemma2(t,S,J,I)))) => lemma2(abs(t),s,i,k)),
(lemma2(t,s,i,k) and lemma2(u,s,i,k) => lemma2(app(t,u),s,i,k)) -> [].




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


/*
Proof:
======

   3 : A<s(A)                                                           [input]
   5 : p(s(A))=A                                                        [input]
   6 : s(p(A))=A                                                        [input]
   8 : s(A)=s(B) -> A=B                                                 [input]
  10 : p(A)<A                                                           [input]
  12 : subst(var(A),A,B)=B                                              [input]
  14 : A=<B,s(B)=<A                                                     [input]
  15 : A=<p(B),B=<A                                                     [input]
  16 : lift(app(A,B),C)=app(lift(A,C),lift(B,C))                        [input]
  17 : lift(abs(A),B)=abs(lift(A,s(B)))                                 [input]
  18 : subst(app(A,B),C,D)=app(subst(A,C,D),subst(B,C,D))               [input]
  19 : subst(abs(A),B,C)=abs(subst(A,s(B),lift(C,0)))                   [input]
  20 : lift(var(A),B)=var(A),B=<A                                       [input]
  21 : lift(var(A),B)=var(s(A)),A<B                                     [input]
  22 : subst(var(A),B,C)=var(A),B=<A                                    [input]
  23 : subst(var(A),B,C)=var(p(A)),A=<B                                 [input]
  25 : A=<B -> s(A)=<s(B)                                               [input]
  27 : lemma1(A,B,C)==(B<s(C)=>lift(lift(A,B),s(C))=lift(lift(A,C),B))  [input]
  28 : 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]
  33 : lemma1(A,B,C)                                                    [input]
  34 + lemma2(var(j),s,i,k),!A,B,C.(lemma2(t,C,A,B))=>lemma2(abs(t),s,i,k),lemma2(t,s,i,k)and lemma2(u,s,i,k)=>lemma2(app(t,u),s,i,k) ->  [input]
  36 : A<B,s(B)=<s(A)                             [totality resolution from 25]
  38 : A<s(B)=>lift(lift(C,A),s(B))=lift(lift(C,B),A) [reduction of 33 by [27]]
  39 : A<s(B) -> lift(lift(C,A),s(B))=lift(lift(C,B),A)     [expansion from 38]
  40 : s(A)=<B,lift(lift(C,B),s(A))=lift(lift(C,A),B) [totality resolution from 39]
  41 + !A,B,C.(A<s(B)and 0=<A=>lift(subst(t,A,C),B)=subst(lift(t,s(B)),A,lift(C,B)))=>i<s(k)and 0=<i=>abs(lift(subst(t,s(i),lift(s,0)),s(k)))=abs(subst(lift(t,s(s(k))),s(i),lift(lift(s,k),0))),i<s(k)and 0=<i=>lift(subst(var(j),i,s),k)=subst(lift(var(j),s(k)),i,lift(s,k)),(i<s(k)and 0=<i=>lift(subst(t,i,s),k)=subst(lift(t,s(k)),i,lift(s,k)))and(i<s(k)and 0=<i=>lift(subst(u,i,s),k)=subst(lift(u,s(k)),i,lift(s,k)))=>i<s(k)and 0=<i=>app(lift(subst(t,i,s),k),lift(subst(u,i,s),k))=app(subst(lift(t,s(k)),i,lift(s,k)),subst(lift(u,s(k)),i,lift(s,k))) ->  [reduction of 34 by [28,28,17,19,19,17,28,28,16,18,18,16,28,28]]
  42 + p$199,i<s(k)and 0=<i=>lift(subst(var(j),i,s),k)=subst(lift(var(j),s(k)),i,lift(s,k)),(i<s(k)and 0=<i=>lift(subst(t,i,s),k)=subst(lift(t,s(k)),i,lift(s,k)))and(i<s(k)and 0=<i=>lift(subst(u,i,s),k)=subst(lift(u,s(k)),i,lift(s,k)))=>i<s(k)and 0=<i=>app(lift(subst(t,i,s),k),lift(subst(u,i,s),k))=app(subst(lift(t,s(k)),i,lift(s,k)),subst(lift(u,s(k)),i,lift(s,k))) ->  [expansion from 41]
  43 + p$199,!A,B,C.(A<s(B)and 0=<A=>lift(subst(t,A,C),B)=subst(lift(t,s(B)),A,lift(C,B))) [expansion from 41]
  44 + i<s(k)and 0=<i=>abs(lift(subst(t,s(i),lift(s,0)),s(k)))=abs(subst(lift(t,s(s(k))),s(i),lift(lift(s,k),0))) -> p$199 [expansion from 41]
  45 + A<s(B),0=<A -> p$199,lift(subst(t,A,C),B)=subst(lift(t,s(B)),A,lift(C,B)) [expansion from 43]
  47 + A<0,s(B)=<A,p$199,lift(subst(t,A,C),B)=subst(lift(t,s(B)),A,lift(C,B)) [totality resolution from 45]
  48 + p$198,i<s(k)and 0=<i=>lift(subst(var(j),i,s),k)=subst(lift(var(j),s(k)),i,lift(s,k)),p$199 ->  [expansion from 42]
  49 + p$198,(i<s(k)and 0=<i=>lift(subst(t,i,s),k)=subst(lift(t,s(k)),i,lift(s,k)))and(i<s(k)and 0=<i=>lift(subst(u,i,s),k)=subst(lift(u,s(k)),i,lift(s,k))) [expansion from 42]
  50 + i<s(k)and 0=<i=>app(lift(subst(t,i,s),k),lift(subst(u,i,s),k))=app(subst(lift(t,s(k)),i,lift(s,k)),subst(lift(u,s(k)),i,lift(s,k))) -> p$198 [expansion from 42]
  51 + p$197 -> p$199                                       [expansion from 44]
  52 + p$197,i<s(k)and 0=<i                                 [expansion from 44]
  53 + abs(lift(subst(t,s(i),lift(s,0)),s(k)))=abs(subst(lift(t,s(s(k))),s(i),lift(lift(s,k),0))) -> p$197 [expansion from 44]
  54 + p$196,p$198,p$199 ->                                 [expansion from 48]
  55 + p$196,i<s(k)and 0=<i                                 [expansion from 48]
  56 + lift(subst(var(j),i,s),k)=subst(lift(var(j),s(k)),i,lift(s,k)) -> p$196 [expansion from 48]
  57 + p$195,p$198                                          [expansion from 49]
  58 + p$195 -> i<s(k)and 0=<i=>lift(subst(t,i,s),k)=subst(lift(t,s(k)),i,lift(s,k)) [expansion from 49]
  59 + p$195 -> i<s(k)and 0=<i=>lift(subst(u,i,s),k)=subst(lift(u,s(k)),i,lift(s,k)) [expansion from 49]
  60 + p$195,i<s(k),0=<i -> lift(subst(t,i,s),k)=subst(lift(t,s(k)),i,lift(s,k)) [expansion from 58]
  62 + p$195 -> i<0,s(k)=<i,lift(subst(t,i,s),k)=subst(lift(t,s(k)),i,lift(s,k)) [totality resolution from 60]
  63 + p$195,i<s(k),0=<i -> lift(subst(u,i,s),k)=subst(lift(u,s(k)),i,lift(s,k)) [expansion from 59]
  65 + p$195 -> i<0,s(k)=<i,lift(subst(u,i,s),k)=subst(lift(u,s(k)),i,lift(s,k)) [totality resolution from 63]
  66 + p$194 -> p$198                                       [expansion from 50]
  67 + p$194,i<s(k)and 0=<i                                 [expansion from 50]
  68 + app(lift(subst(t,i,s),k),lift(subst(u,i,s),k))=app(subst(lift(t,s(k)),i,lift(s,k)),subst(lift(u,s(k)),i,lift(s,k))) -> p$194 [expansion from 50]
  69 + p$193,p$197                                          [expansion from 52]
  70 + p$193 -> i<s(k)                                      [expansion from 52]
  71 + p$193 -> 0=<i                                        [expansion from 52]
  72 + p$193,p$196                                          [expansion from 55]
  73 + p$193,p$194                                          [expansion from 67]
  74 + p$197,0=<i                             [negative chaining of 69 from 71]
  75 + p$197,i<s(k)                           [negative chaining of 69 from 70]
  77 + p$196,i<s(k)                           [negative chaining of 72 from 70]
  78 + p$194,0=<i                             [negative chaining of 73 from 71]
  79 + p$194,i<s(k)                           [negative chaining of 73 from 70]
  80 + i<A,A=<k,p$197                                  [chaining of 14 from 75]
  81 + i<A,A=<k,p$196                                  [chaining of 14 from 77]
  82 + i<A,A=<k,p$194                                  [chaining of 14 from 79]
  83 + p$197,i=<k                                [variable elimination from 80]
  84 + p$196,i=<k                                [variable elimination from 81]
  85 + p$194,i=<k                                [variable elimination from 82]
  89 + i<s(A),A<k,p$197                                [chaining of 36 from 75]
  90 + i<s(A),A<k,p$196                                [chaining of 36 from 77]
  92 + subst(var(j),i,lift(s,k))=lift(subst(var(j),i,s),k) -> s(k)=<j,p$196 [negative chaining of 20 from 56]
  93 + subst(var(s(j)),i,lift(s,k))=lift(subst(var(j),i,s),k) -> j<s(k),p$196 [negative chaining of 21 from 56]
  94 + var(j)=lift(subst(var(j),i,s),k) -> i=<j,s(k)=<j,p$196 [negative chaining of 22 from 92]
  96 + var(j)=lift(var(j),k) -> i=<j,p$196       [reduction of 94 by [22,90,L]]
  97 + k=<j,i=<j,p$196                        [negative chaining of 20 from 96]
 101 + i=<j,p$196,i=<j,p$196                           [chaining of 84 from 97]
 104 + i=<j,p$196                                         [condensement of 101]
 107 + var(p(j))=lift(subst(var(j),i,s),k) -> j=<i,s(k)=<j,p$196 [negative chaining of 23 from 92]
 108 + var(p(s(j)))=lift(subst(var(j),i,s),k) -> s(j)=<i,j<s(k),p$196 [negative chaining of 23 from 93]
 110 + var(p(j))=lift(var(p(j)),k) -> p$196,s(k)=<j,j=i [reduction of 107 by [23,104]]
 111 + var(j)=lift(subst(var(j),i,s),k) -> p$196,j<s(k),s(j)=i [reduction of 108 by [5,3,104]]
 112 + k=<p(j),p$196,s(k)=<j,j=i             [negative chaining of 20 from 110]
 115 + k<j,p$196,j=i,k=<p(j)                           [chaining of 3 from 112]
 124 + k=<p(j),j=i,p$196                             [reduction of 115 by [15]]
 131 + k<j,j=i,p$196                                  [chaining of 10 from 124]
 139 + lift(var(p(j)),k)=var(j) -> j=<i,p$196,j<s(k),s(j)=i [negative chaining of 23 from 111]
 140 + s(j)=i,j<s(k),p$196,j=i         [reduction of 139 by [21,124,L,6,L,104]]
 141 + j<A,A=<k,p$196,j=i,s(j)=i                      [chaining of 14 from 140]
 145 + j=i,s(j)=i,p$196,j=<k                    [variable elimination from 141]
 146 + j=i,s(j)=i,p$196,j=k                         [reduction of 145 by [131]]
 148 + j<i,p$196,j=i,k=j                               [chaining of 3 from 146]
 165 + j=<i,p$196,k=j                                     [condensement of 148]
 166 + k=j,p$196,j=i                                [reduction of 165 by [104]]
 181 + subst(lift(var(j),s(k)),i,lift(s,j))=lift(subst(var(j),i,s),k) -> p$196,j=i,p$196 [negative chaining of 166 from 56]
 202 + subst(lift(var(j),s(k)),i,lift(s,j))=lift(subst(var(j),i,s),k) -> j=i,p$196 [condensement of 181]
 203 + p$196,j=i [reduction of 202 by [166,20,3,L,23,104,166,23,104,20,10,L,L]]
 215 + subst(var(i),i,lift(s,k))=lift(subst(var(j),i,s),k) -> p$196,s(k)=<j,p$196 [negative chaining of 203 from 92]
 227 + subst(var(i),i,lift(s,k))=lift(subst(var(j),i,s),k) -> s(k)=<j,p$196 [condensement of 215]
 228 + p$196,s(k)=i                  [reduction of 227 by [12,203,12,L,203,77]]
 241 + k<i,p$196                                       [chaining of 3 from 228]
 263 + p$196                                       [reduction of 241 by [84,L]]
 270 + p$199,p$198 ->                                [reduction of 54 by [263]]
 271 + p$198,subst(lift(t,s(k)),i,lift(s,k))=lift(subst(t,i,s),k),i<0,s(k)=<i [negative chaining of 57 from 62]
 272 + p$198,subst(lift(t,s(k)),i,lift(s,k))=lift(subst(t,i,s),k),s(k)=i [reduction of 271 by [78,66,L,L,79,66,L]]
 275 + p$198,subst(lift(u,s(k)),i,lift(s,k))=lift(subst(u,i,s),k),i<0,s(k)=<i [negative chaining of 57 from 65]
 276 + p$198,subst(lift(u,s(k)),i,lift(s,k))=lift(subst(u,i,s),k),s(k)=i [reduction of 275 by [78,66,L,L,79,66,L]]
 277 + app(subst(lift(t,s(k)),i,lift(s,k)),lift(subst(u,i,s),k))=app(lift(subst(t,i,s),k),lift(subst(u,i,s),k)) -> p$198,s(k)=i,p$194 [negative chaining of 276 from 68]
 279 + p$198,s(k)=i                          [reduction of 277 by [272,L,66,L]]
 281 + k<i,p$198                                       [chaining of 3 from 279]
 300 + p$198                                  [reduction of 281 by [85,66,L,L]]
 304 + p$199 ->                                     [reduction of 270 by [300]]
 305 + subst(lift(t,s(A)),B,lift(C,A))=lift(subst(t,B,C),A),s(A)=<B,B<0 [reduction of 47 by [304,L]]
 306 + p$197 ->                                    [reduction of 51 by [304,L]]
 308 + 0=<i                                        [reduction of 74 by [306,L]]
 310 + i=<k                                        [reduction of 83 by [306,L]]
 312 + i<s(A),A<k                                  [reduction of 89 by [306,L]]
 313 + abs(subst(lift(t,s(s(k))),s(i),lift(lift(s,k),0)))=abs(lift(subst(t,s(i),lift(s,0)),s(k))) ->  [reduction of 53 by [306,L]]
 317 + abs(subst(lift(t,s(s(k))),s(i),lift(lift(s,0),s(k))))=abs(lift(subst(t,s(i),lift(s,0)),s(k))) -> s(k)=<0 [negative chaining of 40 from 313]
 318 + abs(subst(lift(t,s(s(k))),s(i),lift(lift(s,0),s(k))))=abs(lift(subst(t,s(i),lift(s,0)),s(k))) -> s(k)=0 [reduction of 317 by [312,308]]
 319 + s(s(k))=<s(i),s(i)<0,s(k)=0          [negative chaining of 305 from 318]
 320 + s(k)=i,s(k)=0                 [reduction of 319 by [36,312,L,8,3,308,L]]
 324 + k<i,k<0                                         [chaining of 3 from 320]
 342 + false                            [reduction of 324 by [310,L,310,308,L]]

Length = 121, Depth = 41



Total time: 20930 milliseconds

Number of forward inferences: 170
Number of tableau inferences: 23
Number of kept clauses: 94

*/