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

% Proof by induction over S
% base case
lemmaF1(var(j),c,d,i),

% step case for abstractions
(all(I,all(C,lemmaF1(s,C,d,I))) => lemmaF1(abs(s),c,d,i)),

% step case for applications
(lemmaF1(s,c,d,i) and lemmaF1(t,c,d,i) => lemmaF1(app(s,t),c,d,i)) -> [].

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


/*
Proof:
======

  11 : A<s(A)                                                           [input]
  14 : A<B -> subst(var(B),A,C)=var(p(B))                               [input]
  16 : A<B -> subst(var(A),B,C)=var(A)                                  [input]
  17 : subst(app(A,B),C,D)=app(subst(A,C,D),subst(B,C,D))               [input]
  18 : subst(abs(A),B,C)=abs(subst(A,s(B),lift(C,0)))                   [input]
  23 : free(var(A),B)==(A=B)                                            [input]
  24 : free(app(A,B),C)==(free(A,C)or free(B,C))                        [input]
  25 : free(abs(A),B)==free(A,s(B))                                     [input]
  35 : lemmaF1(A,B,C,D)==(~free(A,D)and 0=<D=>subst(A,D,B)=subst(A,D,C)) [input]
  36 : lemmaF1(var(j),c,d,i),!A,B.(lemmaF1(s,B,d,A))=>lemmaF1(abs(s),c,d,i),lemmaF1(s,c,d,i)and lemmaF1(t,c,d,i)=>lemmaF1(app(s,t),c,d,i) ->  [input]
  39 : A=<B,subst(var(A),B,C)=var(p(A))           [totality resolution from 14]
  40 : A=<B,subst(var(B),A,C)=var(B)              [totality resolution from 16]
  46 : !A,B.(~free(s,A)and 0=<A=>subst(s,A,B)=subst(s,A,d))=> ~free(s,s(i))and 0=<i=>abs(subst(s,s(i),lift(c,0)))=abs(subst(s,s(i),lift(d,0))),~ (j=i)and 0=<i=>subst(var(j),i,c)=subst(var(j),i,d),(~free(s,i)and 0=<i=>subst(s,i,c)=subst(s,i,d))and(~free(t,i)and 0=<i=>subst(t,i,c)=subst(t,i,d))=> ~ (free(s,i)or free(t,i))and 0=<i=>app(subst(s,i,c),subst(t,i,c))=app(subst(s,i,d),subst(t,i,d)) ->  [reduction of 36 by [35,23,35,18,18,25,35,35,17,17,24,35,35]]
  47 : p$199,~ (j=i)and 0=<i=>subst(var(j),i,c)=subst(var(j),i,d),!A,B.(~free(s,A)and 0=<A=>subst(s,A,B)=subst(s,A,d))=> ~free(s,s(i))and 0=<i=>abs(subst(s,s(i),lift(c,0)))=abs(subst(s,s(i),lift(d,0))) ->  [expansion from 46]
  48 : p$199,(~free(s,i)and 0=<i=>subst(s,i,c)=subst(s,i,d))and(~free(t,i)and 0=<i=>subst(t,i,c)=subst(t,i,d)) [expansion from 46]
  49 : ~ (free(s,i)or free(t,i))and 0=<i=>app(subst(s,i,c),subst(t,i,c))=app(subst(s,i,d),subst(t,i,d)) -> p$199 [expansion from 46]
  50 : p$198,~ (j=i)and 0=<i=>subst(var(j),i,c)=subst(var(j),i,d),p$199 ->  [expansion from 47]
  51 : p$198,!A,B.(~free(s,A)and 0=<A=>subst(s,A,B)=subst(s,A,d)) [expansion from 47]
  52 : ~free(s,s(i))and 0=<i=>abs(subst(s,s(i),lift(c,0)))=abs(subst(s,s(i),lift(d,0))) -> p$198 [expansion from 47]
  53 : 0=<A -> p$198,subst(s,A,B)=subst(s,A,d),free(s,A)    [expansion from 51]
  54 : A<0,p$198,subst(s,A,B)=subst(s,A,d),free(s,A) [totality resolution from 53]
  55 : p$197,p$199                                          [expansion from 48]
  56 : p$197 -> ~free(s,i)and 0=<i=>subst(s,i,c)=subst(s,i,d) [expansion from 48]
  57 : p$197 -> ~free(t,i)and 0=<i=>subst(t,i,c)=subst(t,i,d) [expansion from 48]
  58 : p$197,0=<i -> subst(s,i,c)=subst(s,i,d),free(s,i)    [expansion from 56]
  59 : p$197 -> i<0,subst(s,i,c)=subst(s,i,d),free(s,i) [totality resolution from 58]
  60 : p$197,0=<i -> subst(t,i,c)=subst(t,i,d),free(t,i)    [expansion from 57]
  61 : p$197 -> i<0,subst(t,i,c)=subst(t,i,d),free(t,i) [totality resolution from 60]
  62 : p$196 -> p$199                                       [expansion from 49]
  63 : p$196,~ (free(s,i)or free(t,i))and 0=<i              [expansion from 49]
  64 : app(subst(s,i,c),subst(t,i,c))=app(subst(s,i,d),subst(t,i,d)) -> p$196 [expansion from 49]
  65 : p$195 -> p$198                                       [expansion from 52]
  66 : p$195,~free(s,s(i))and 0=<i                          [expansion from 52]
  67 : abs(subst(s,s(i),lift(c,0)))=abs(subst(s,s(i),lift(d,0))) -> p$195 [expansion from 52]
  68 : p$194,p$196                                          [expansion from 63]
  69 : p$194 -> ~ (free(s,i)or free(t,i))                   [expansion from 63]
  70 : p$194 -> 0=<i                                        [expansion from 63]
  71 : p$194,free(s,i)or free(t,i) ->                       [expansion from 69]
  72 : p$193,p$195                                          [expansion from 66]
  73 : p$193 -> ~free(s,s(i))                               [expansion from 66]
  74 : p$193 -> 0=<i                                        [expansion from 66]
  75 : p$193,free(s,s(i)) ->                                [expansion from 73]
  76 : p$192,p$194 ->                                       [expansion from 71]
  77 : free(s,i) -> p$192                                   [expansion from 71]
  78 : free(t,i) -> p$192                                   [expansion from 71]
  79 : p$196,0=<i                             [negative chaining of 68 from 70]
  80 : p$195,0=<i                             [negative chaining of 72 from 74]
  81 : p$199,free(s,i),i<0,subst(s,i,d)=subst(s,i,c) [negative chaining of 55 from 59]
  82 : p$199,subst(s,i,d)=subst(s,i,c) [reduction of 81 by [77,76,68,62,L,L,L,79,62,L,L]]
  85 : p$199,free(t,i),i<0,subst(t,i,d)=subst(t,i,c) [negative chaining of 55 from 61]
  86 : p$199,subst(t,i,d)=subst(t,i,c) [reduction of 85 by [78,76,68,62,L,L,L,79,62,L,L]]
  87 : app(subst(s,i,d),subst(t,i,c))=app(subst(s,i,c),subst(t,i,c)) -> p$199,p$196 [negative chaining of 86 from 64]
  89 : p$199                                   [reduction of 87 by [82,L,62,L]]
  91 : ~ (j=i)and 0=<i=>subst(var(j),i,c)=subst(var(j),i,d),p$198 ->  [reduction of 50 by [89]]
  92 : p$191,p$198 ->                                       [expansion from 91]
  93 : p$191,~ (j=i)and 0=<i                                [expansion from 91]
  94 : subst(var(j),i,c)=subst(var(j),i,d) -> p$191         [expansion from 91]
  95 : p$190,p$191                                          [expansion from 93]
  96 : p$190 -> ~ (j=i)                                     [expansion from 93]
  98 : p$190,j=i ->                                         [expansion from 96]
  99 : j=i -> p$191                           [negative chaining of 95 from 98]
 101 : var(j)=subst(var(j),i,c) -> i=<j,p$191 [negative chaining of 40 from 94]
 102 : var(p(j))=subst(var(j),i,c) -> j=<i,p$191 [negative chaining of 39 from 94]
 103 : p$191,i=<j                                  [reduction of 101 by [40,L]]
 104 : p$191                              [reduction of 102 by [39,L,103,99,L]]
 105 : p$198 ->                                      [reduction of 92 by [104]]
 106 : subst(s,A,B)=subst(s,A,d),free(s,A),A<0     [reduction of 54 by [105,L]]
 107 : p$195 ->                                    [reduction of 65 by [105,L]]
 108 : p$193                                       [reduction of 72 by [107,L]]
 109 : 0=<i                                        [reduction of 80 by [107,L]]
 110 : abs(subst(s,s(i),lift(d,0)))=abs(subst(s,s(i),lift(c,0))) ->  [reduction of 67 by [107,L]]
 111 : free(s,s(i)) ->                               [reduction of 75 by [108]]
 114 : subst(s,s(i),A)=subst(s,s(i),d),s(i)<0 {[conj([free(s,s(i))>A],[],[])]} [negative chaining of 106 from 111]
 116 : subst(s,s(i),A)=subst(s,s(i),d) {[conj([free(s,s(i))>A],[],[])]} [reduction of 114 by [11,109,L]]
 117 : false                                  [reduction of 110 by [116,116,L]]

Length = 75, Depth = 23



Total time: 44810 milliseconds

Number of forward inferences: 13
Number of tableau inferences: 30
Number of kept clauses: 87
*/