---

Step * of Lemma code-seq1_wf

∀[k:ℕ]. ∀[s:ℕk ⟶ ℕ].  (code-seq1(k;s) ∈ ℕ)
BY
{ xxxProveWfLemmaxxx }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[s:\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}].    (code-seq1(k;s)  \mmember{}  \mBbbN{})


By

---

Latex:
xxxProveWfLemmaxxx

---

Home Index