---

Step * of Lemma code-pair-bijection

Bij(ℕ;ℕ × ℕ;λx.coded-pair(x))
BY
{ xxx(RepeatFor 2 ((D 0 THEN Auto)) THEN All Reduce)xxx }

1
1. a1 : ℕ
2. a2 : ℕ
3. coded-pair(a1) = coded-pair(a2) ∈ (ℕ × ℕ)
⊢ a1 = a2 ∈ ℕ

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

---

Latex:

---

Latex:
Bij(\mBbbN{};\mBbbN{}  \mtimes{}  \mBbbN{};\mlambda{}x.coded-pair(x))


By

---

Latex:
xxx(RepeatFor  2  ((D  0  THEN  Auto))  THEN  All  Reduce)xxx

---

Home Index