---

Step * 1 2 1 1 1 1 1 of Lemma integer-sqrt-bin-search


1. x : ℕ@i
2. ¬x < 2
3. (iroot(2;x)^2 ≤ x) ∧ x < iroot(2;x) + 1^2
⊢ ((iroot(2;x) * iroot(2;x)) ≤ x) ∧ x < (iroot(2;x) + 1) * (iroot(2;x) + 1)
BY
{ (Unfold `exp` -1 THEN (RWO "primrec-unroll" (-1) THENA Auto) THEN Reduce (-1) THEN Auto') }

---

Latex:

---

Latex:

1.  x  :  \mBbbN{}@i
2.  \mneg{}x  <  2
3.  (iroot(2;x)\^{}2  \mleq{}  x)  \mwedge{}  x  <  iroot(2;x)  +  1\^{}2
\mvdash{}  ((iroot(2;x)  *  iroot(2;x))  \mleq{}  x)  \mwedge{}  x  <  (iroot(2;x)  +  1)  *  (iroot(2;x)  +  1)


By

---

Latex:
(Unfold  `exp`  -1  THEN  (RWO  "primrec-unroll"  (-1)  THENA  Auto)  THEN  Reduce  (-1)  THEN  Auto')

---

Home Index