use(subst).
use(beta).
use(eta).
use(subst_lemmas).

lemmaF1(S,T,U,I).
lemma6(T,I).

etas(S,T) -> etas(abs(S),abs(T)).
betar(S,T) == (beta(S,T) or S=T).

goal

(~free(abs(s),0) =>
   (beta(abs(app(abs(s),var(0))),abs(subst(s,0,var(0)))) and
     eta(abs(app(abs(s),var(0))),subst(abs(s),0,x)) and
        (abs(subst(s,0,var(0)))=G) and
   betar(subst(abs(s),0,x),G) )) -> [].

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


/*
Proof:
======

  11 : A<s(A)                                                           [input]
  18 : subst(abs(A),B,C)=abs(subst(A,s(B),lift(C,0)))                   [input]
  25 : free(abs(A),B)==free(A,s(B))                                     [input]
  26 : beta(app(abs(A),B),subst(A,0,B))                                 [input]
  29 : beta(A,B) -> beta(abs(A),abs(B))                                 [input]
  33 : ~free(A,0) -> eta(abs(app(A,var(0))),subst(A,0,B))               [input]
  45 : lemma6(A,B)==(0=<B=>subst(A,B,var(B))=subst(A,s(B),var(B)))      [input]
  46 : lemmaF1(A,B,C,D)==(~free(A,D)and 0=<D and~B=C=>subst(A,D,B)=subst(A,D,C)) [input]
  47 : lemmaF1(A,B,C,D)                                                 [input]
  48 : lemma6(A,B)                                                      [input]
  50 : betar(A,B)==(beta(A,B)or A=B)                                    [input]
  51 + ~free(abs(s),0)=>beta(abs(app(abs(s),var(0))),abs(subst(s,0,var(0))))and eta(abs(app(abs(s),var(0))),subst(abs(s),0,x))and abs(subst(s,0,var(0)))=A and betar(subst(abs(s),0,x),A) ->  [input]
  59 : eta(abs(app(A,var(0))),subst(A,0,B)),free(A,0)       [expansion from 33]
  61 + ~free(s,s(0))=>eta(abs(app(abs(s),var(0))),subst(abs(s),0,x))and abs(subst(s,0,var(0)))=A and(beta(subst(abs(s),0,x),A)or subst(abs(s),0,x)=A) ->  [reduction of 51 by [50,29,26,L,25]]
  62 : 0=<A=>subst(B,A,var(A))=subst(B,s(A),var(A))   [reduction of 45 by [48]]
  63 : 0=<A -> subst(B,A,var(A))=subst(B,s(A),var(A))       [expansion from 62]
  64 : A<0,subst(B,A,var(A))=subst(B,s(A),var(A)) [totality resolution from 63]
  65 : ~free(A,B)and 0=<B and~C=D=>subst(A,B,C)=subst(A,B,D) [reduction of 46 by [47]]
  66 : 0=<A -> subst(B,A,C)=subst(B,A,D),C=D,free(B,A)      [expansion from 65]
  67 : A<0,subst(B,A,C)=subst(B,A,D),C=D,free(B,A) [totality resolution from 66]
  95 + ~free(s,s(0))                                        [expansion from 61]
  96 + eta(abs(app(abs(s),var(0))),subst(abs(s),0,x))and abs(subst(s,0,var(0)))=A and(beta(subst(abs(s),0,x),A)or subst(abs(s),0,x)=A) ->  [expansion from 61]
  97 + free(s,s(0)) ->                                      [expansion from 95]
  98 + abs(subst(s,0,var(0)))=A and(beta(subst(abs(s),0,x),A)or subst(abs(s),0,x)=A) ->  [reduction of 96 by [59,25,97,L,L]]
  99 + abs(subst(s,0,var(0)))=A,beta(subst(abs(s),0,x),A)or subst(abs(s),0,x)=A ->  [expansion from 98]
 112 + p$195(A),abs(subst(s,0,var(0)))=A ->                 [expansion from 99]
 114 + subst(abs(s),0,x)=A -> p$195(A)                      [expansion from 99]
 120 + p$195(abs(subst(s,0,var(0)))) ->       [reflexivity resolution from 112]
 121 + p$195(subst(abs(s),0,x))               [reflexivity resolution from 114]
 122 + p$195(abs(subst(s,s(0),lift(x,0)))) {[conj([subst(abs(s),0,x)>abs(subst(s,s(0),lift(x,0)))],[],[])]} [chaining of 18 from 121]
 123 + p$195(abs(subst(s,s(0),var(0)))) ->  {[conj([subst(s,0,var(0))>subst(s,s(0),var(0))],[],[])]} [negative chaining of 64 from 120]
 130 + p$195(abs(subst(s,s(0),A))) -> s(0)<0,var(0)=A,free(s,s(0)) {[conj([subst(s,0,var(0))>subst(s,s(0),var(0)),subst(s,s(0),var(0))>subst(s,s(0),A)],[],[])]} [negative chaining of 67 from 123]
 134 + p$195(abs(subst(s,s(0),A))) -> var(0)=A {[conj([subst(s,0,var(0))>subst(s,s(0),var(0)),subst(s,s(0),var(0))>subst(s,s(0),A)],[],[])]} [reduction of 130 by [11,L,97,L]]
 135 + var(0)=lift(x,0) {[conj([subst(s,0,var(0))>subst(s,s(0),var(0)),subst(s,s(0),var(0))>subst(s,s(0),lift(x,0)),subst(abs(s),0,x)>abs(subst(s,s(0),lift(x,0)))],[],[])]} [negative chaining of 122 from 134]
 139 + p$195(abs(subst(s,s(0),var(0)))) {[conj([subst(s,0,var(0))>subst(s,s(0),var(0)),subst(s,s(0),var(0))>subst(s,s(0),lift(x,0)),subst(abs(s),0,x)>abs(subst(s,s(0),lift(x,0)))],[],[])]} [chaining of 135 from 122]
 296 + false {[conj([subst(s,0,var(0))>subst(s,s(0),var(0)),subst(s,s(0),var(0))>subst(s,s(0),lift(x,0)),subst(abs(s),0,x)>abs(subst(s,s(0),lift(x,0)))],[],[])]} [negative chaining of 139 from 123]

Length = 36, Depth = 14



Total time: 117540 milliseconds

Number of forward inferences: 138
Number of tableau inferences: 46
Number of kept clauses: 219
*/