---

Step * of Lemma code-pair-bijection

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

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

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

---

Latex:

---

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


By

---

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

---

Home Index