---

Step * of Lemma A-loop_wf

∀[Val:Type]. ∀[n:ℕ]. ∀[AType:array{i:l}(Val;n)].
  ∀lo:ℕn. ∀k:ℕ.  (k < n - lo ⇒ (∀[body:{lo..lo + k-} ⟶ (A-map Unit)]. (A-loop(AType;lo;lo + k;body) ∈ A-map Unit)))
BY
{ Auto }

1
1. Val : Type
2. n : ℕ
3. AType : array{i:l}(Val;n)
4. lo : ℕn
5. k : ℕ
6. k < n - lo
7. body : {lo..lo + k-} ⟶ (A-map Unit)
⊢ A-loop(AType;lo;lo + k;body) ∈ A-map Unit

---

Latex:

---

Latex:
\mforall{}[Val:Type].  \mforall{}[n:\mBbbN{}].  \mforall{}[AType:array\{i:l\}(Val;n)].
    \mforall{}lo:\mBbbN{}n.  \mforall{}k:\mBbbN{}.
        (k  <  n  -  lo
        {}\mRightarrow{}  (\mforall{}[body:\{lo..lo  +  k\msupminus{}\}  {}\mrightarrow{}  (A-map  Unit)].  (A-loop(AType;lo;lo  +  k;body)  \mmember{}  A-map  Unit)))


By

---

Latex:
Auto

---

Home Index