---

Step * of Lemma tsqrt_wf

∀[n:ℕ]. (tsqrt(n) ∈ ℕ)
BY
{ xxx((D 0 THENA Auto) THEN Unfold `tsqrt` 0 THEN (GenConclAtAddr [2;1] THENA Auto))xxx }

1
1. n : ℕ
2. v : ℕ
3. isqrt(2 * n) = v ∈ ℕ
⊢ eval r = v in
  if (r * r) + r ≤z 2 * n then r else r - 1 fi  ∈ ℕ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (tsqrt(n)  \mmember{}  \mBbbN{})


By

---

Latex:
xxx((D  0  THENA  Auto)  THEN  Unfold  `tsqrt`  0  THEN  (GenConclAtAddr  [2;1]  THENA  Auto))xxx

---

Home Index