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



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

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

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




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

:-sarp(+[15]).
:-saci([2]).


/*


Proof:
======

   3 : A<s(A)                                                           [input]
  12 : subst(var(A),A,B)=B                                              [input]
  14 : A=<B,s(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]
  21 : lift(var(A),B)=var(s(A)),A<B                                     [input]
  24 : A<B -> s(A)<s(B)                                                 [input]
  25 : lemma1(A,B,C)==(B<s(C)=>lift(lift(A,B),s(C))=lift(lift(A,C),B))  [input]
  27 : lemma3(A,B,C,D)==(C<s(D)and 0=<C=>lift(subst(A,D,B),C)=subst(lift(A,C),s(D),lift(B,C))) [input]
  28 : lemma1(A,B,C)                                                    [input]
  29 + lemma3(var(k),s,i,k),!A,B,C.(lemma3(t,C,A,B))=>lemma3(abs(t),s,i,k),lemma3(t,s,i,k)and lemma3(u,s,i,k)=>lemma3(app(t,u),s,i,k) ->  [input]
  30 : A=<B,s(B)<s(A)                             [totality resolution from 24]
  31 : A<s(B)=>lift(lift(C,A),s(B))=lift(lift(C,B),A) [reduction of 28 by [25]]
  32 : A<s(B) -> lift(lift(C,A),s(B))=lift(lift(C,B),A)     [expansion from 31]
  33 : s(A)=<B,lift(lift(C,B),s(A))=lift(lift(C,A),B) [totality resolution from 32]
  34 + !A,B,C.(A<s(B)and 0=<A=>lift(subst(t,B,C),A)=subst(lift(t,A),s(B),lift(C,A)))=>i<s(k)and 0=<i=>abs(lift(subst(t,s(k),lift(s,0)),s(i)))=abs(subst(lift(t,s(i)),s(s(k)),lift(lift(s,i),0))),i<s(k)and 0=<i=>lift(s,i)=subst(lift(var(k),i),s(k),lift(s,i)),(i<s(k)and 0=<i=>lift(subst(t,k,s),i)=subst(lift(t,i),s(k),lift(s,i)))and(i<s(k)and 0=<i=>lift(subst(u,k,s),i)=subst(lift(u,i),s(k),lift(s,i)))=>i<s(k)and 0=<i=>app(lift(subst(t,k,s),i),lift(subst(u,k,s),i))=app(subst(lift(t,i),s(k),lift(s,i)),subst(lift(u,i),s(k),lift(s,i))) ->  [reduction of 29 by [27,12,27,17,19,19,17,27,27,16,18,18,16,27,27]]
  35 + p$199,i<s(k)and 0=<i=>lift(s,i)=subst(lift(var(k),i),s(k),lift(s,i)),(i<s(k)and 0=<i=>lift(subst(t,k,s),i)=subst(lift(t,i),s(k),lift(s,i)))and(i<s(k)and 0=<i=>lift(subst(u,k,s),i)=subst(lift(u,i),s(k),lift(s,i)))=>i<s(k)and 0=<i=>app(lift(subst(t,k,s),i),lift(subst(u,k,s),i))=app(subst(lift(t,i),s(k),lift(s,i)),subst(lift(u,i),s(k),lift(s,i))) ->  [expansion from 34]
  36 + p$199,!A,B,C.(A<s(B)and 0=<A=>lift(subst(t,B,C),A)=subst(lift(t,A),s(B),lift(C,A))) [expansion from 34]
  37 + i<s(k)and 0=<i=>abs(lift(subst(t,s(k),lift(s,0)),s(i)))=abs(subst(lift(t,s(i)),s(s(k)),lift(lift(s,i),0))) -> p$199 [expansion from 34]
  38 + A<s(B),0=<A -> p$199,lift(subst(t,B,C),A)=subst(lift(t,A),s(B),lift(C,A)) [expansion from 36]
  40 + A<0,s(B)=<A,p$199,lift(subst(t,B,C),A)=subst(lift(t,A),s(B),lift(C,A)) [totality resolution from 38]
  41 + p$198,i<s(k)and 0=<i=>lift(s,i)=subst(lift(var(k),i),s(k),lift(s,i)),p$199 ->  [expansion from 35]
  42 + p$198,(i<s(k)and 0=<i=>lift(subst(t,k,s),i)=subst(lift(t,i),s(k),lift(s,i)))and(i<s(k)and 0=<i=>lift(subst(u,k,s),i)=subst(lift(u,i),s(k),lift(s,i))) [expansion from 35]
  43 + i<s(k)and 0=<i=>app(lift(subst(t,k,s),i),lift(subst(u,k,s),i))=app(subst(lift(t,i),s(k),lift(s,i)),subst(lift(u,i),s(k),lift(s,i))) -> p$198 [expansion from 35]
  44 + p$197 -> p$199                                       [expansion from 37]
  45 + p$197,i<s(k)and 0=<i                                 [expansion from 37]
  46 + abs(lift(subst(t,s(k),lift(s,0)),s(i)))=abs(subst(lift(t,s(i)),s(s(k)),lift(lift(s,i),0))) -> p$197 [expansion from 37]
  47 + p$196,p$198,p$199 ->                                 [expansion from 41]
  48 + p$196,i<s(k)and 0=<i                                 [expansion from 41]
  49 + lift(s,i)=subst(lift(var(k),i),s(k),lift(s,i)) -> p$196 [expansion from 41]
  50 + p$195,p$198                                          [expansion from 42]
  51 + p$195 -> i<s(k)and 0=<i=>lift(subst(t,k,s),i)=subst(lift(t,i),s(k),lift(s,i)) [expansion from 42]
  52 + p$195 -> i<s(k)and 0=<i=>lift(subst(u,k,s),i)=subst(lift(u,i),s(k),lift(s,i)) [expansion from 42]
  53 + p$195,i<s(k),0=<i -> lift(subst(t,k,s),i)=subst(lift(t,i),s(k),lift(s,i)) [expansion from 51]
  55 + p$195 -> i<0,s(k)=<i,lift(subst(t,k,s),i)=subst(lift(t,i),s(k),lift(s,i)) [totality resolution from 53]
  56 + p$195,i<s(k),0=<i -> lift(subst(u,k,s),i)=subst(lift(u,i),s(k),lift(s,i)) [expansion from 52]
  58 + p$195 -> i<0,s(k)=<i,lift(subst(u,k,s),i)=subst(lift(u,i),s(k),lift(s,i)) [totality resolution from 56]
  59 + p$194 -> p$198                                       [expansion from 43]
  60 + p$194,i<s(k)and 0=<i                                 [expansion from 43]
  61 + app(lift(subst(t,k,s),i),lift(subst(u,k,s),i))=app(subst(lift(t,i),s(k),lift(s,i)),subst(lift(u,i),s(k),lift(s,i))) -> p$194 [expansion from 43]
  62 + p$193,p$197                                          [expansion from 45]
  63 + p$193 -> i<s(k)                                      [expansion from 45]
  64 + p$193 -> 0=<i                                        [expansion from 45]
  65 + p$193,p$196                                          [expansion from 48]
  66 + p$193,p$194                                          [expansion from 60]
  67 + p$197,0=<i                             [negative chaining of 62 from 64]
  68 + p$197,i<s(k)                           [negative chaining of 62 from 63]
  70 + p$196,i<s(k)                           [negative chaining of 65 from 63]
  71 + p$194,0=<i                             [negative chaining of 66 from 64]
  72 + p$194,i<s(k)                           [negative chaining of 66 from 63]
  74 + i<A,A=<k,p$196                                  [chaining of 14 from 70]
  77 + p$196,i=<k                                [variable elimination from 74]
  83 + subst(var(s(k)),s(k),lift(s,i))=lift(s,i) -> k<i,p$196 [negative chaining of 21 from 49]
  84 + p$196                                   [reduction of 83 by [12,L,77,L]]
  85 + p$199,p$198 ->                                 [reduction of 47 by [84]]
  86 + p$198,subst(lift(t,i),s(k),lift(s,i))=lift(subst(t,k,s),i),i<0,s(k)=<i [negative chaining of 50 from 55]
  87 + s(k)=<i,i<0,subst(lift(t,i),s(k),lift(s,i))=lift(subst(t,k,s),i) [reduction of 86 by [85,40,L]]
  90 + p$198,subst(lift(u,i),s(k),lift(s,i))=lift(subst(u,k,s),i),i<0,s(k)=<i [negative chaining of 50 from 58]
  91 + p$198,subst(lift(u,i),s(k),lift(s,i))=lift(subst(u,k,s),i) [reduction of 90 by [71,59,L,L,72,59,L,L]]
  92 + app(subst(lift(t,i),s(k),lift(s,i)),lift(subst(u,k,s),i))=app(lift(subst(t,k,s),i),lift(subst(u,k,s),i)) -> p$198,p$194 [negative chaining of 91 from 61]
  94 + p$198                         [reduction of 92 by [87,71,L,72,L,L,59,L]]
  95 + p$199 ->                                       [reduction of 85 by [94]]
  96 + subst(lift(t,A),s(B),lift(C,A))=lift(subst(t,B,C),A),s(B)=<A,A<0 [reduction of 40 by [95,L]]
  97 + p$197 ->                                     [reduction of 44 by [95,L]]
  99 + 0=<i                                         [reduction of 67 by [97,L]]
 100 + i<s(k)                                       [reduction of 68 by [97,L]]
 103 + abs(subst(lift(t,s(i)),s(s(k)),lift(lift(s,i),0)))=abs(lift(subst(t,s(k),lift(s,0)),s(i))) ->  [reduction of 46 by [97,L]]
 109 + abs(subst(lift(t,s(i)),s(s(k)),lift(lift(s,0),s(i))))=abs(lift(subst(t,s(k),lift(s,0)),s(i))) -> s(i)=<0 [negative chaining of 33 from 103]
 110 + s(i)=0                      [reduction of 109 by [96,30,100,L,L,L,3,99]]
 112 + i<0                                             [chaining of 3 from 110]
 122 + false                                       [reduction of 112 by [99,L]]

Length = 73, Depth = 20



Total time: 15600 milliseconds

Number of forward inferences: 33
Number of tableau inferences: 23
Number of kept clauses: 60

*/