---

Step * of Lemma finite-sequence-coding-exists

∃code:ℕ ⟶ (k:ℕ × (ℕk ⟶ ℕ)). Surj(ℕ;k:ℕ × (ℕk ⟶ ℕ);code)
BY
{ xxx(With ⌜λn.coded-seq(n)⌝ (D 0)⋅ THEN Auto THEN (D 0 THEN Auto) THEN D -1 THEN Reduce 0)xxx }

1
1. k : ℕ
2. b1 : ℕk ⟶ ℕ
⊢ ∃a:ℕ. (coded-seq(a) = <k, b1> ∈ (k:ℕ × (ℕk ⟶ ℕ)))

---

Latex:

---

Latex:
\mexists{}code:\mBbbN{}  {}\mrightarrow{}  (k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{})).  Surj(\mBbbN{};k:\mBbbN{}  \mtimes{}  (\mBbbN{}k  {}\mrightarrow{}  \mBbbN{});code)


By

---

Latex:
xxx(With  \mkleeneopen{}\mlambda{}n.coded-seq(n)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  (D  0  THEN  Auto)  THEN  D  -1  THEN  Reduce  0)xxx

---

Home Index