---

Step * 1 of Lemma pair-coding-exists


1. b : ℕ × ℕ
⊢ ∃a:ℕ. (coded-pair(a) = b ∈ (ℕ × ℕ))
BY
{ xxx(D -1 THEN With ⌜code-pair(b1;b2)⌝ (D 0)⋅ THEN Auto)xxx }

---

Latex:

---

Latex:

1.  b  :  \mBbbN{}  \mtimes{}  \mBbbN{}
\mvdash{}  \mexists{}a:\mBbbN{}.  (coded-pair(a)  =  b)


By

---

Latex:
xxx(D  -1  THEN  With  \mkleeneopen{}code-pair(b1;b2)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)xxx

---

Home Index