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



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

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

goal
lemma4(var(j),s,k),
(all(K,all(S,lemma4(t,S,K))) => lemma4(abs(t),s,k)),
(lemma4(t,s,k) and lemma4(u,s,k) => lemma4(app(t,u),s,k)) -> [].




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


/*

Proof:
======

   3 : A<s(A)                                                           [input]
   5 : p(s(A))=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]
  28 : lemma4(A,B,C)==(subst(lift(A,C),C,B)=A)                          [input]
  29 + lemma4(var(j),s,k),!A,B.(lemma4(t,B,A))=>lemma4(abs(t),s,k),lemma4(t,s,k)and lemma4(u,s,k)=>lemma4(app(t,u),s,k) ->  [input]
  31 + !A,B.(subst(lift(t,A),A,B)=t)=>abs(subst(lift(t,s(k)),s(k),lift(s,0)))=abs(t),subst(lift(var(j),k),k,s)=var(j),subst(lift(t,k),k,s)=t and subst(lift(u,k),k,s)=u=>app(subst(lift(t,k),k,s),subst(lift(u,k),k,s))=app(t,u) ->  [reduction of 29 by [28,L,28,17,19,28,28,16,18,28,28]]
  32 + p$199,!A,B.(subst(lift(t,A),A,B)=t)=>abs(subst(lift(t,s(k)),s(k),lift(s,0)))=abs(t),subst(lift(var(j),k),k,s)=var(j) ->  [expansion from 31]
  33 + p$199,subst(lift(t,k),k,s)=t and subst(lift(u,k),k,s)=u [expansion from 31]
  34 + app(subst(lift(t,k),k,s),subst(lift(u,k),k,s))=app(t,u) -> p$199 [expansion from 31]
  35 + p$198,subst(lift(var(j),k),k,s)=var(j),p$199 ->      [expansion from 32]
  36 + p$198,!A,B.(subst(lift(t,A),A,B)=t)                  [expansion from 32]
  37 + abs(subst(lift(t,s(k)),s(k),lift(s,0)))=abs(t) -> p$198 [expansion from 32]
  38 + p$198,subst(lift(t,A),A,B)=t                         [expansion from 36]
  39 + p$198                                        [reduction of 37 by [38,L]]
  40 + subst(lift(var(j),k),k,s)=var(j),p$199 ->      [reduction of 35 by [39]]
  41 + p$197,p$199                                          [expansion from 33]
  42 + p$197 -> subst(lift(t,k),k,s)=t                      [expansion from 33]
  43 + p$197 -> subst(lift(u,k),k,s)=u                      [expansion from 33]
  44 + p$199,subst(lift(t,k),k,s)=t           [negative chaining of 41 from 42]
  45 + p$199,subst(lift(u,k),k,s)=u           [negative chaining of 41 from 43]
  46 + app(t,subst(lift(u,k),k,s))=app(t,u) -> p$199,p$199 [negative chaining of 44 from 34]
  48 + app(t,subst(lift(u,k),k,s))=app(t,u) -> p$199       [condensement of 46]
  49 + p$199                                        [reduction of 48 by [45,L]]
  51 + subst(lift(var(j),k),k,s)=var(j) ->            [reduction of 40 by [49]]
  52 + subst(var(j),k,s)=var(j) -> k=<j       [negative chaining of 20 from 51]
  53 + k=<j                                         [reduction of 52 by [22,L]]
  54 + subst(var(s(j)),k,s)=var(j) -> j<k     [negative chaining of 21 from 51]
  55 + false                          [reduction of 54 by [23,53,3,L,5,L,53,L]]

Length = 35, Depth = 12



Total time: 3070 milliseconds

Number of forward inferences: 6
Number of tableau inferences: 9
Number of kept clauses: 22

*/