---

Step * of Lemma callbyvalueall-seq-extend-2

∀[F,G,L,K:Top]. ∀[m:ℕ+]. ∀[n:ℕm + 1].
  (callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λout.let x ⟵ F[out]
                                                             in G[x];m - 1);n;m) 
  ~ callbyvalueall-seq(λn.if (n =z m) then mk_lambdas(λx.F[x];m - 1) else L n fi ;λf.mk_applies(f;K;n)
                       ;mk_lambdas(λx.G[x];m);n;m + 1))
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ⌜∃i:ℕ. (m = (n + i) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
   THEN ExRepD
   THEN HypSubst' (-1) 0
   THEN RepeatFor 2 ((D (-3) THENA Auto))
   THEN DVar `m'
   THEN (HypSubst' (-1) (-6) THENA Auto)
   THEN ThinVar `m'
   THEN MoveToConcl (-4)
   THEN MoveToConcl (-2)
   THEN NatInd (-1)) }

1
.....basecase..... 
1. F : Top
2. G : Top
3. L : Top
4. i : ℤ
⊢ ∀K:Top. ∀n:ℤ.
    ((0 ≤ n)
    ⇒ 0 < n + 0
    ⇒ (callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λout.let x ⟵ F[out]
                                                                  in G[x];(n + 0) - 1);n;n + 0) 
       ~ callbyvalueall-seq(λn@0.if (n@0 =z n + 0) then mk_lambdas(λx.F[x];(n + 0) - 1) else L n@0 fi 
                            ;λf.mk_applies(f;K;n);mk_lambdas(λx.G[x];n + 0);n;(n + 0) + 1)))

2
.....upcase..... 
1. F : Top
2. G : Top
3. L : Top
4. i : ℤ
5. 0 < i
6. ∀K:Top. ∀n:ℤ.
     ((0 ≤ n)
     ⇒ 0 < n + (i - 1)
     ⇒ (callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λout.let x ⟵ F[out]
                                                                   in G[x];(n + (i - 1)) - 1);n;n + (i - 1)) 
        ~ callbyvalueall-seq(λn@0.if (n@0 =z n + (i - 1)) then mk_lambdas(λx.F[x];(n + (i - 1)) - 1) else L n@0 fi 
                             ;λf.mk_applies(f;K;n);mk_lambdas(λx.G[x];n + (i - 1));n;(n + (i - 1)) + 1)))
⊢ ∀K:Top. ∀n:ℤ.
    ((0 ≤ n)
    ⇒ 0 < n + i
    ⇒ (callbyvalueall-seq(L;λf.mk_applies(f;K;n);mk_lambdas(λout.let x ⟵ F[out]
                                                                  in G[x];(n + i) - 1);n;n + i) 
       ~ callbyvalueall-seq(λn@0.if (n@0 =z n + i) then mk_lambdas(λx.F[x];(n + i) - 1) else L n@0 fi 
                            ;λf.mk_applies(f;K;n);mk_lambdas(λx.G[x];n + i);n;(n + i) + 1)))

---

Latex:

---

Latex:
\mforall{}[F,G,L,K:Top].  \mforall{}[m:\mBbbN{}\msupplus{}].  \mforall{}[n:\mBbbN{}m  +  1].
    (callbyvalueall-seq(L;\mlambda{}f.mk\_applies(f;K;n);mk\_lambdas(\mlambda{}out.let  x  \mleftarrow{}{}  F[out]
                                                                                                                          in  G[x];m  -  1);n;m) 
    \msim{}  callbyvalueall-seq(\mlambda{}n.if  (n  =\msubz{}  m)  then  mk\_lambdas(\mlambda{}x.F[x];m  -  1)  else  L  n  fi 
                                              ;\mlambda{}f.mk\_applies(f;K;n);mk\_lambdas(\mlambda{}x.G[x];m);n;m  +  1))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}i:\mBbbN{}.  (m  =  (n  +  i))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  ExRepD
  THEN  HypSubst'  (-1)  0
  THEN  RepeatFor  2  ((D  (-3)  THENA  Auto))
  THEN  DVar  `m'
  THEN  (HypSubst'  (-1)  (-6)  THENA  Auto)
  THEN  ThinVar  `m'
  THEN  MoveToConcl  (-4)
  THEN  MoveToConcl  (-2)
  THEN  NatInd  (-1))

---

Home Index