---

Step * of Lemma callbyvalueall-seq_wf

∀[T:Type]. ∀[m:ℕ]. ∀[n:ℕm + 1]. ∀[A:ℕm ⟶ ValueAllType]. ∀[L:i:ℕm ⟶ funtype(i;A;A i)]. ∀[G:∀[T:Type]
                                                                                              (funtype(n;A;T) ⟶ T)].
∀[F:funtype(m;A;T)].
  (callbyvalueall-seq(L;G;F;n;m) ∈ T)
BY
{ (Unfold `vatype` 0
   THEN Auto
   THEN (DVar `n' THENA Auto)
   THEN (Assert ⌜∃k:ℕ. (n = (m - k) ∈ ℤ)⌝⋅ THENA (InstConcl [⌜m - n⌝]⋅ THEN Auto'))
   THEN ExRepD
   THEN Eliminate ⌜n⌝⋅
   THEN ThinVar `n'
   THEN NatInd 2
   THEN Try ((Subst ⌜m - 0 ~ m⌝ 0⋅ THENA Auto))
   THEN Auto
   THEN RecUnfold `callbyvalueall-seq` 0
   THEN AutoSplit
   THEN Try (Complete ((Subst ⌜m - k ~ m⌝ (-2)⋅ THEN Auto')))
   THEN (D (-4) THENA Auto)
   THEN (Subst ⌜m - k - 1 ~ (m - k) + 1⌝ (-1)⋅ THENA Auto)
   THEN GenConclAtAddr [2;1]
   THEN Auto
   THEN BackThruSomeHyp) }

1
1. m : ℕ
2. T : Type
3. A : ℕm ⟶ {T:Type| valueall-type(T)} 
4. L : i:ℕm ⟶ funtype(i;A;A i)
5. F : funtype(m;A;T)
6. k : ℤ
7. ¬(m ≤ (m - k))
8. 0 < k
9. 0 ≤ (m - k)
10. m - k < m + 1
11. G : ∀[T:Type]. (funtype(m - k;A;T) ⟶ T)
12. ∀G:∀[T:Type]. (funtype((m - k) + 1;A;T) ⟶ T). (callbyvalueall-seq(L;G;F;(m - k) + 1;m) ∈ T)
13. v : A (m - k)
14. (G (L (m - k))) = v ∈ (A (m - k))
15. T1 : Type
16. f : funtype((m - k) + 1;A;T1)
⊢ G f v ∈ T1

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[m:\mBbbN{}].  \mforall{}[n:\mBbbN{}m  +  1].  \mforall{}[A:\mBbbN{}m  {}\mrightarrow{}  ValueAllType].  \mforall{}[L:i:\mBbbN{}m  {}\mrightarrow{}  funtype(i;A;A  i)].
\mforall{}[G:\mforall{}[T:Type].  (funtype(n;A;T)  {}\mrightarrow{}  T)].  \mforall{}[F:funtype(m;A;T)].
    (callbyvalueall-seq(L;G;F;n;m)  \mmember{}  T)


By

---

Latex:
(Unfold  `vatype`  0
  THEN  Auto
  THEN  (DVar  `n'  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}\mexists{}k:\mBbbN{}.  (n  =  (m  -  k))\mkleeneclose{}\mcdot{}  THENA  (InstConcl  [\mkleeneopen{}m  -  n\mkleeneclose{}]\mcdot{}  THEN  Auto'))
  THEN  ExRepD
  THEN  Eliminate  \mkleeneopen{}n\mkleeneclose{}\mcdot{}
  THEN  ThinVar  `n'
  THEN  NatInd  2
  THEN  Try  ((Subst  \mkleeneopen{}m  -  0  \msim{}  m\mkleeneclose{}  0\mcdot{}  THENA  Auto))
  THEN  Auto
  THEN  RecUnfold  `callbyvalueall-seq`  0
  THEN  AutoSplit
  THEN  Try  (Complete  ((Subst  \mkleeneopen{}m  -  k  \msim{}  m\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto')))
  THEN  (D  (-4)  THENA  Auto)
  THEN  (Subst  \mkleeneopen{}m  -  k  -  1  \msim{}  (m  -  k)  +  1\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  GenConclAtAddr  [2;1]
  THEN  Auto
  THEN  BackThruSomeHyp)

---

Home Index