---

Step * of Lemma callbyvalueall_seq_wf

∀[T,U: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) ⟶ T) ⟶ U].
  (callbyvalueall_seq(L;G;F;n;m) ∈ U)
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)) }

1
1. m : ℕ
2. T : Type
3. U : Type
4. A : ℕm ⟶ {T:Type| valueall-type(T)} 
5. L : i:ℕm ⟶ funtype(i;A;A i)
6. F : (funtype(m;A;T) ⟶ T) ⟶ U
7. k : ℤ
8. ¬(m ≤ (m - k))
9. 0 < k
10. 0 ≤ (m - k)
11. m - k < m + 1
12. G : ∀[T:Type]. (funtype(m - k;A;T) ⟶ T)
13. ∀G:∀[T:Type]. (funtype((m - k) + 1;A;T) ⟶ T). (callbyvalueall_seq(L;G;F;(m - k) + 1;m) ∈ U)
⊢ let v ⟵ G (L (m - k))
  in callbyvalueall_seq(L;λf.(G f v);F;(m - k) + 1;m) ∈ U

---

Latex:

---

Latex:
\mforall{}[T,U: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)  {}\mrightarrow{}  T)  {}\mrightarrow{}  U].
    (callbyvalueall\_seq(L;G;F;n;m)  \mmember{}  U)


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))

---

Home Index