---

Step * of Lemma coded-seq_wf

∀x:ℕ. (coded-seq(x) ∈ k:ℕ × (ℕk ⟶ ℕ))
BY
{ TACTIC:ProveWfLemma }

---

Latex:

---

Latex:
\mforall{}x:\mBbbN{}.  (coded-seq(x)  \mmember{}  k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{}))


By

---

Latex:
TACTIC:ProveWfLemma

---

Home Index