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.
155def modelIntegerRoot =
156 (lambda unrestricted value : Nat .
157 (app
158 (nat-eliminate
159 (lambda unrestricted current : Nat . (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)))
160 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat . low))
161 (lambda unrestricted predecessor : Nat .
162 (lambda unrestricted induction : (pi unrestricted low : Nat . (pi unrestricted high : Nat . Nat)) .
163 (lambda unrestricted low : Nat . (lambda unrestricted high : Nat .
164 (specSelect (nat-less-than (nat-add low 1) high)
165 (specSelect (nat-less-than value (nat-multiply (nat-divide (nat-add low high) 2) (nat-divide (nat-add low high) 2)))
166 (induction low (nat-divide (nat-add low high) 2))
167 (induction (nat-divide (nat-add low high) 2) high))
168 low)))))
169 200)
170 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.