---

Step * 2 of Lemma code-pair-bijection


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

---

Latex:

---

Latex:

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


By

---

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

---

Home Index