---

Step * of Lemma coded-pair_wf

∀[n:ℕ]. (coded-pair(n) ∈ ℕ × ℕ)
BY
{ ((Auto THEN Unfold `coded-pair` 0) THEN RepeatFor 4 ((CallByValueReduce 0 THENA Auto))) }

1
1. n : ℕ
⊢ <n - t(tsqrt(n)), tsqrt(n) - n - t(tsqrt(n))> ∈ ℕ × ℕ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (coded-pair(n)  \mmember{}  \mBbbN{}  \mtimes{}  \mBbbN{})


By

---

Latex:
((Auto  THEN  Unfold  `coded-pair`  0)  THEN  RepeatFor  4  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index