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



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

% induction proof for lemma6(T,I)

goal
lemma6(var(j),i),
(all(K,lemma6(t,K)) => lemma6(abs(t),i)),
(lemma6(t,i) and lemma6(u,i) => lemma6(app(t,u),i)) -> [].




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


/*
Proof:
======

   3 : A<s(A)                                                           [input]
   5 : p(s(A))=A                                                        [input]
  12 : subst(var(A),A,B)=B                                              [input]
  14 : A=<B,s(B)=<A                                                     [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]
  22 : subst(var(A),B,C)=var(A),B=<A                                    [input]
  23 : subst(var(A),B,C)=var(p(A)),A=<B                                 [input]
  37 : lemma6(A,B)==(0=<B=>subst(A,B,var(B))=subst(A,s(B),var(B)))      [input]
  38 + lemma6(var(j),i),!A.(lemma6(t,A))=>lemma6(abs(t),i),lemma6(t,i)and lemma6(u,i)=>lemma6(app(t,u),i) ->  [input]
  42 + !A.(0=<A=>subst(t,A,var(A))=subst(t,s(A),var(A)))=>0=<i=>abs(subst(t,s(i),lift(var(i),0)))=abs(subst(t,s(s(i)),lift(var(i),0))),0=<i=>subst(var(j),i,var(i))=subst(var(j),s(i),var(i)),(0=<i=>subst(t,i,var(i))=subst(t,s(i),var(i)))and(0=<i=>subst(u,i,var(i))=subst(u,s(i),var(i)))=>0=<i=>app(subst(t,i,var(i)),subst(u,i,var(i)))=app(subst(t,s(i),var(i)),subst(u,s(i),var(i))) ->  [reduction of 38 by [37,37,19,19,37,37,18,18,37,37]]
  43 + p$199,0=<i=>subst(var(j),i,var(i))=subst(var(j),s(i),var(i)),(0=<i=>subst(t,i,var(i))=subst(t,s(i),var(i)))and(0=<i=>subst(u,i,var(i))=subst(u,s(i),var(i)))=>0=<i=>app(subst(t,i,var(i)),subst(u,i,var(i)))=app(subst(t,s(i),var(i)),subst(u,s(i),var(i))) ->  [expansion from 42]
  44 + p$199,!A.(0=<A=>subst(t,A,var(A))=subst(t,s(A),var(A))) [expansion from 42]
  45 + 0=<i=>abs(subst(t,s(i),lift(var(i),0)))=abs(subst(t,s(s(i)),lift(var(i),0))) -> p$199 [expansion from 42]
  46 + 0=<A -> p$199,subst(t,A,var(A))=subst(t,s(A),var(A)) [expansion from 44]
  47 + A<0,p$199,subst(t,A,var(A))=subst(t,s(A),var(A)) [totality resolution from 46]
  48 + p$198,0=<i=>subst(var(j),i,var(i))=subst(var(j),s(i),var(i)),p$199 ->  [expansion from 43]
  49 + p$198,(0=<i=>subst(t,i,var(i))=subst(t,s(i),var(i)))and(0=<i=>subst(u,i,var(i))=subst(u,s(i),var(i))) [expansion from 43]
  50 + 0=<i=>app(subst(t,i,var(i)),subst(u,i,var(i)))=app(subst(t,s(i),var(i)),subst(u,s(i),var(i))) -> p$198 [expansion from 43]
  51 + p$197 -> p$199                                       [expansion from 45]
  52 + p$197,0=<i                                           [expansion from 45]
  53 + abs(subst(t,s(i),lift(var(i),0)))=abs(subst(t,s(s(i)),lift(var(i),0))) -> p$197 [expansion from 45]
  54 + abs(subst(t,s(i),var(s(i))))=abs(subst(t,s(s(i)),var(s(i)))) -> p$197 [reduction of 53 by [21,52,L,21,52,L]]
  55 + p$196,p$198,p$199 ->                                 [expansion from 48]
  57 + subst(var(j),i,var(i))=subst(var(j),s(i),var(i)) -> p$196 [expansion from 48]
  58 + p$195,p$198                                          [expansion from 49]
  59 + p$195 -> 0=<i=>subst(t,i,var(i))=subst(t,s(i),var(i)) [expansion from 49]
  60 + p$195 -> 0=<i=>subst(u,i,var(i))=subst(u,s(i),var(i)) [expansion from 49]
  61 + p$195,0=<i -> subst(t,i,var(i))=subst(t,s(i),var(i)) [expansion from 59]
  62 + p$195 -> i<0,subst(t,i,var(i))=subst(t,s(i),var(i)) [totality resolution from 61]
  63 + p$195,0=<i -> subst(u,i,var(i))=subst(u,s(i),var(i)) [expansion from 60]
  64 + p$195 -> i<0,subst(u,i,var(i))=subst(u,s(i),var(i)) [totality resolution from 63]
  65 + p$194 -> p$198                                       [expansion from 50]
  66 + p$194,0=<i                                           [expansion from 50]
  67 + app(subst(t,i,var(i)),subst(u,i,var(i)))=app(subst(t,s(i),var(i)),subst(u,s(i),var(i))) -> p$194 [expansion from 50]
  68 + p$198,subst(t,s(i),var(i))=subst(t,i,var(i)),i<0 [negative chaining of 58 from 62]
  69 + p$198,subst(t,s(i),var(i))=subst(t,i,var(i)) [reduction of 68 by [66,65,L,L]]
  70 + p$198,subst(u,s(i),var(i))=subst(u,i,var(i)),i<0 [negative chaining of 58 from 64]
  71 + p$198,subst(u,s(i),var(i))=subst(u,i,var(i)) [reduction of 70 by [66,65,L,L]]
  72 + app(subst(t,i,var(i)),subst(u,s(i),var(i)))=app(subst(t,i,var(i)),subst(u,i,var(i))) -> p$198,p$194 [negative chaining of 69 from 67]
  74 + p$198                                   [reduction of 72 by [71,L,65,L]]
  75 + p$196,p$199 ->                                 [reduction of 55 by [74]]
  76 + p$199,s(i)<0,p$197                     [negative chaining of 47 from 54]
  78 + p$199                                 [reduction of 76 by [3,52,L,51,L]]
  79 + p$196 ->                                       [reduction of 75 by [78]]
  81 + subst(var(j),s(i),var(i))=subst(var(j),i,var(i)) ->  [reduction of 57 by [79,L]]
  84 + var(j)=subst(var(j),i,var(i)) -> s(i)=<j [negative chaining of 22 from 81]
  85 + i=<j,s(i)=<j                           [negative chaining of 22 from 84]
  86 + s(i)=<j,i=j                                    [reduction of 85 by [14]]
  87 + var(p(j))=subst(var(j),i,var(i)) -> j=<s(i) [negative chaining of 23 from 81]
  90 + j=<i,j=<s(i)                           [negative chaining of 23 from 87]
  92 + j=<i,j=s(i)                                    [reduction of 90 by [86]]
  93 + s(i)=<i,j=i,j=s(i)                              [chaining of 86 from 92]
  94 + j=s(i),j=i                                    [reduction of 93 by [3,L]]
  98 + subst(var(s(i)),s(i),var(i))=subst(var(j),i,var(i)) -> j=i [negative chaining of 94 from 81]
 102 + j=i                              [reduction of 98 by [12,94,23,3,L,5,L]]
 103 + false                         [reduction of 81 by [102,22,3,L,102,12,L]]

Length = 58, Depth = 23



Total time: 5150 milliseconds

Number of forward inferences: 19
Number of tableau inferences: 18
Number of kept clauses: 51

*/