---

Step * of Lemma code-seq1_wf

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

---

Latex:

---

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


By

---

Latex:
TACTIC:ProveWfLemma

---

Home Index