---

Step * of Lemma code-seq_wf

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

---

Latex:

---

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


By

---

Latex:
xxxxxxProveWfLemmaxxxxxx

---

Home Index