square root: NaN quieted; signed zero preserved; +inf; a negative operand is
invalid. A finite value is M / 2^150 with M the scaled magnitude, so its
root is sqrt(M * 2^150) / 2^150 with an integer radicand of even scale; the
floor root q is exact when q*q = N, and otherwise (2q+1)/2^151 lies on the
same side of every rounding boundary as the true root.
261def modelIntegerRoot =
262 (lambda unrestricted value : Nat .
263 (app
264 (nat-eliminate
265 (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)))
266 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low))
267 (lambda unrestricted predecessor : Nat .
268 (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) .
269 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
270 (specSelect (nat-less-than (nat-add low 1) high)
271 (specSelect (nat-less-than value (nat-multiply (nat-divide (nat-add low high) 2) (nat-divide (nat-add low high) 2)))
272 (induction low (nat-divide (nat-add low high) 2))
273 (induction (nat-divide (nat-add low high) 2) high))
274 low)))))
275 200)
276 zero (specPow2 (nat-add (nat-divide (specBitLength value) 2) 2))))The compiler supplied declaration spans and resolved links from this source snapshot. This page does not assert that this file belongs to a checked closure.