---

Step * of Lemma pair-coding-exists

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

1
1. b : ℕ × ℕ
⊢ ∃a:ℕ. (coded-pair(a) = b ∈ (ℕ × ℕ))

---

Latex:

---

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


By

---

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

---

Home Index