~/bend-docscommunity

proofs/math/typed/f64sqc.bend checks

raw source on the hub · import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64sqc.bend as F64sqc

25 imports
import Base
import ./f64light.bend as FL
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../spec/math/w64.bend as SW
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../../src/math/u64.bend as WU
import ../../../src/math/natural.bend as M
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../natural/arith.bend as NR
import ../natural/sqrtn.bend as SQ2
import ./width.bend as WW
import ./natcmp.bend as NC
import ./w64add.bend as WA
import ./w64sh.bend as SH
import ./f64bits.bend as FB
import ./f64cmp.bend as FC
import ./f64round.bend as FR
import ./f64rtools.bend as RT
import ./f64norm.bend as NM
import ./f64mexp.bend as EX
import ./f64sqf.bend as QF

Definitions

def m01 source · line 32 · raw

@+m:Nat -> @+hl:{Nat.is_lt(m, 2n) == True{} : Bool} -> @+h:{Nat.is_eq(m, 1n) == False{} : Bool} -> {m == 0n : Nat}

def m10 source · line 43 · raw

@+m:Nat -> @+hl:{Nat.is_lt(m, 2n) == True{} : Bool} -> @+h:{Nat.is_eq(m, 0n) == False{} : Bool} -> {m == 1n : Nat}

def halve_c source · line 54 · raw

@+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(Nat.add(x, x), Nat.add(y, y)) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_le(x, y) == c : Bool} -> {c == True{} : Bool}

def halve source · line 62 · raw

@+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(Nat.add(x, x), Nat.add(y, y)) == True{} : Bool} -> {Nat.is_le(x, y) == True{} : Bool}

def two_add source · line 65 · raw

@+a:Nat -> {Nat.add(Nat.mul(a, 2n), 0n) == Nat.add(a, a) : Nat}

def div_dbl source · line 68 · raw

@+p:Nat -> {Nat.div(Nat.add(p, p), 2n) == p : Nat}

def half_eq source · line 72 · raw

@+n:Nat -> {n == Nat.add(Nat.add(Nat.div(n, 2n), Nat.div(n, 2n)), Nat.mod(n, 2n)) : Nat}

n = 2 * (n / 2) + (n mod 2)

def jperm source · line 76 · raw

@+b:Nat -> @+K:Nat -> @+D:Nat -> @+p:Nat -> @+s:Nat -> {Nat.add(Nat.add(Nat.add(Nat.add(b, Nat.add(K, D)), Nat.add(b, Nat.add(K, D))), p), s) == Nat.add(Nat.add(b, b), Nat.add(Nat.add(Nat.add(K, K), p), Nat.add(Nat.add(D, D), s))) : Nat}

(b + (K + D)) twice, then p, then s, regrouped

def jfg source · line 101 · raw

@+a:Nat -> @+b:Nat -> @+sa:Nat -> @+p:Nat -> @+q:Nat -> @+K:Nat -> @+u:Nat -> @+hEN2:{Nat.add(Nat.add(Nat.add(a, a), p), sa) == Nat.add(Nat.add(Nat.add(b, b), q), 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> @+hp:{Nat.is_le(p, 1n) == True{} : Bool} -> @+hK:{Nat.is_le(K, 1022n) == True{} : Bool} -> @+hKu:{Nat.add(Nat.add(K, K), p) == Nat.add(2043n, u) : Nat} -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), K), Nat.sub(Nat.sub(a, b), K)), Nat.add(72n, Nat.add(sa, u))) == Nat.add(200n, q) : Nat}

the exponent step of sqn_c for any parity: 2a + p + s = 2b + q + 2171 with s <= 53, p <= 1, K <= 1022 and 2K + p = 2043 + u gives 2 ((a - b) - K) + 72 + s + u = 200 + q

def jf00 source · line 136 · raw

@+a:Nat -> @+b:Nat -> @+sa:Nat -> @+hEN2:{Nat.add(Nat.add(Nat.add(a, a), 0n), sa) == Nat.add(Nat.add(Nat.add(b, b), 0n), 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1022n), Nat.sub(Nat.sub(a, b), 1022n)), Nat.add(72n, Nat.add(sa, 1n))) == Nat.add(200n, 0n) : Nat}

def jf01 source · line 139 · raw

@+a:Nat -> @+b:Nat -> @+sa:Nat -> @+hEN2:{Nat.add(Nat.add(Nat.add(a, a), 0n), sa) == Nat.add(Nat.add(Nat.add(b, b), 1n), 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1022n), Nat.sub(Nat.sub(a, b), 1022n)), Nat.add(72n, Nat.add(sa, 1n))) == Nat.add(200n, 1n) : Nat}

def jf10 source · line 142 · raw

@+a:Nat -> @+b:Nat -> @+sa:Nat -> @+hEN2:{Nat.add(Nat.add(Nat.add(a, a), 1n), sa) == Nat.add(Nat.add(Nat.add(b, b), 0n), 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1021n), Nat.sub(Nat.sub(a, b), 1021n)), Nat.add(72n, Nat.add(sa, 0n))) == Nat.add(200n, 0n) : Nat}

def jf11 source · line 145 · raw

@+a:Nat -> @+b:Nat -> @+sa:Nat -> @+hEN2:{Nat.add(Nat.add(Nat.add(a, a), 1n), sa) == Nat.add(Nat.add(Nat.add(b, b), 1n), 2171n) : Nat} -> @+hsa:{Nat.is_le(sa, 53n) == True{} : Bool} -> {Nat.add(Nat.add(Nat.sub(Nat.sub(a, b), 1021n), Nat.sub(Nat.sub(a, b), 1021n)), Nat.add(72n, Nat.add(sa, 0n))) == Nat.add(200n, 1n) : Nat}

def sqn_c_g1 source · line 148 · raw

@+av0_:Nat -> @+eEN:{av0_ == Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 1n) : Nat} -> {Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n) == Nat.add(av0_, 4096n) : Nat}

def sqn_c_g2 source · line 151 · raw

@+av0_:Nat -> @+hp:{Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1511n), Nat.add(Nat.div(av0_, 2n), 1511n)), 1075n) == Nat.add(av0_, 4096n) : Nat} -> {Nat.div(Nat.sub(Nat.add(av0_, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1075n), 2n) == Nat.add(Nat.div(av0_, 2n), 1511n) : Nat}

def sqn_c_g3 source · line 154 · raw

@+av0_:Nat -> @+eEN:{av0_ == Nat.add(Nat.add(Nat.div(av0_, 2n), Nat.div(av0_, 2n)), 0n) : Nat} -> @+hE:{Nat.add(Nat.sub(av0_, 1n), 1n) == av0_ : Nat} -> {Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n) == Nat.add(Nat.sub(av0_, 1n), 4096n) : Nat}

def sqn_c_g4 source · line 157 · raw

@+av0_:Nat -> @+hp:{Nat.add(Nat.add(Nat.add(Nat.div(av0_, 2n), 1510n), Nat.add(Nat.div(av0_, 2n), 1510n)), 1075n) == Nat.add(Nat.sub(av0_, 1n), 4096n) : Nat} -> {Nat.div(Nat.sub(Nat.add(Nat.sub(av0_, 1n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1075n), 2n) == Nat.add(Nat.div(av0_, 2n), 1510n) : Nat}

def sqn_t source · line 162 · raw

@+e:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(e, m, True{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(e, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1075n), 2n), 1048n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(m, 8n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

sq_n on a known parity, unfolded once over variables (the four cases of sqn_c rewrite with these instead of unfolding the square root each time)

def sqn_f source · line 165 · raw

@+e:Nat -> @+m:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(e, m, False{}) == 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_root(Nat.add(Nat.div(Nat.sub(Nat.add(Nat.sub(e, 1n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.off), 1075n), 2n), 1048n), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.shl(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.add(m, m), 8n)) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sqn_c source · line 168 · raw

@+xl:U32 -> @+xh:U32 -> @+hzx:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n)) == False{} : Bool} -> @+o:Bool -> @+ho:{Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 2n), 1n) == o : Bool} -> @+ev:Bool -> @+hev:{Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2n), 0n) == ev : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), o) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, ev, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sqrt_even(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sqrt_even(Nat.mul(2n, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.mant(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), Nat.sub(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.xexp(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sqfin source · line 267 · raw

@+xl:U32 -> @+xh:U32 -> @+hzx:{Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n)) == False{} : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 2n), 1n)) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sqrt_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def simpl source · line 270 · raw

@+s:Bool -> @+a:Bool -> @+b:Bool -> @+c:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def sspec source · line 273 · raw

@+s:Bool -> @+a:Bool -> @+b:Bool -> @+c:Bool -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64

def ssh3 source · line 276 · raw

@+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+s:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_pos(e, f, s) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(e, f), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(e, f), Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(e, f), 2n), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ssh2 source · line 283 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+s:Bool -> @+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+z:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_sign(x, s, e, f, z) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, z, x, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, s, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.nan, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(e, f), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(e, f), Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(e, f), 2n), 1n)))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ssh1 source · line 290 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+s:Bool -> @+e:Nat -> @+f:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/u64.U64 -> @+t:Bool -> {0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_cls(x, s, e, f, t) == simpl(s, t, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/w64.is_zero(f), Nat.is_eq(e, 0n), x, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(e, f), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(e, f), Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(e, f), 2n), 1n))) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def ne2047 source · line 297 · raw

@+E:Nat -> {Bool.and(Nat.is_eq(E, 2047n), Nat.is_eq(E, 0n)) == False{} : Bool}

def sswap source · line 304 · raw

@+s1:Bool -> @+s2:Bool -> @+hs:{s1 == s2 : Bool} -> @+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+p1:Bool -> @+q1:Bool -> @+h0:{p1 == q1 : Bool} -> @+p2:Bool -> @+q2:Bool -> @+h1:{p2 == q2 : Bool} -> @+p3:Bool -> @+q3:Bool -> @+h2:{p3 == q3 : Bool} -> {simpl(s1, p1, p2, p3, x, r) == simpl(s2, q1, q2, q3, x, r) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def scase source · line 307 · raw

@+xl:U32 -> @+xh:U32 -> @+r1:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+r2:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> @+aq:Bool -> @+ha:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n) == aq : Bool} -> @+bq:Bool -> @+cq:Bool -> @+hc:{Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n) == cq : Bool} -> @+ngv:Bool -> @+hR:{0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, Bool.or(Bool.or(aq, Bool.and(cq, bq)), ngv), r2, r1) == r2 : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64} -> {simpl(ngv, aq, bq, cq, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, r1) == sspec(ngv, aq, bq, cq, 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}, r2) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sR_c source · line 342 · raw

@+xl:U32 -> @+xh:U32 -> @+g:Bool -> @+hg:{Bool.or(Bool.or(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.efield(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n), Nat.is_eq(0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0n))), 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sign(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})) == g : Bool} -> {0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.pick(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64, g, 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sqrt_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.sq_n(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_f(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), Nat.is_eq(Nat.mod(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.norm_e(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.exp_field(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}), 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.frac(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh})), 2n), 1n))) == 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.sqrt_fin(0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.Bits{xl, xh}) : 0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64}

def sqrt_value source · line 350 · raw

@+x:0xf86f5f1d9a594d5a5cff999100e01d03/src/math/f64.F64 -> 0xf86f5f1d9a594d5a5cff999100e01d03/spec/math/f64.Sqrt.value(x)