---

Step * 1 of Lemma tsqrt_wf


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  ∈ ℕ
BY
{ ((CallByValueReduce 0 THENA Auto) THEN OldAutoSplit) }

1
1. n : ℕ
2. v : ℕ
3. isqrt(2 * n) = v ∈ ℕ
4. 2 * n < (v * v) + v
⊢ v - 1 ∈ ℕ

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  v  :  \mBbbN{}
3.  isqrt(2  *  n)  =  v
\mvdash{}  eval  r  =  v  in
    if  (r  *  r)  +  r  \mleq{}z  2  *  n  then  r  else  r  -  1  fi    \mmember{}  \mBbbN{}


By

---

Latex:
((CallByValueReduce  0  THENA  Auto)  THEN  OldAutoSplit)

---

Home Index