def sR_c

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64sqc.bend:342

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

342def sR_c(+xl: U32, +xh: U32, +g: Bool, +hg: {Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), SF.sign(F.Bits{xl, xh})) == g : Bool}) -> {SF.pick(F.F64, g, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))) == SF.sqrt_fin(F.Bits{xl, xh}) : F.F64}:
343  match g:
344    case True{}:
345      Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), SF.sqrt_fin(F.Bits{xl, xh}), SF.sqrt_fin(F.Bits{xl, xh}), FR.pk_t(F.F64, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), {==})
346    case False{}:
347      +h1 = FC.or_l(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), SF.sign(F.Bits{xl, xh}), hg)
348      Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n)), SF.sqrt_fin(F.Bits{xl, xh}), FR.pk_f(F.F64, SF.sqrt_fin(F.Bits{xl, xh}), F.sq_n(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), F.norm_f(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), Nat.is_eq(Nat.mod(F.norm_e(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), 2n), 1n))), sqfin(xl, xh, FC.or_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), h1)))