def sqrt_value

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

import Base
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
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/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

350def sqrt_value(+x: F.F64) -> SF.Sqrt.value(x):
351  match x:
352    case F.Bits{+xl, +xh}:
353      +i1 = ssh1(F.Bits{xl, xh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n))
354      +i2 = sswap(F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh}), 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)), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 2047n), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), FL.hea(xl, xh)), X.is_zero(F.frac(F.Bits{xl, xh})), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), FB.fz_g(xl, xh, 1048575, {==}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), FL.hea(xl, xh)))
355      +i3 = scase(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}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), {==}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), {==}, SF.sign(F.Bits{xl, xh}), sR_c(xl, xh, 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})), {==}))
356      Equal.trans(F.F64, F.sq_cls(F.Bits{xl, xh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), simpl(SF.sign(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 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))), sspec(SF.sign(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), F.Bits{xl, xh}, SF.sqrt_fin(F.Bits{xl, xh})), Equal.trans(F.F64, F.sq_cls(F.Bits{xl, xh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), simpl(F.signbit(F.Bits{xl, xh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n), X.is_zero(F.frac(F.Bits{xl, xh})), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 0n), 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))), simpl(SF.sign(F.Bits{xl, xh}), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), 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))), i1, i2), i3)