def yp_eq

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64divc.bend:67

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/spec/math/w64.bend as SW
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/lib/nat.bend as N
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/f64norm.bend as NM

67def yp_eq(+yl: U32, +yh: U32, +hzy: {Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)) == False{} : Bool}) -> {SF.mant(F.Bits{yl, yh}) == 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n) : Nat}:
68  +n1 = NM.n1(1n, {==}, F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{yl, yh}), hea(yl, yh), hfr(yl, yh), FC.hF(yl, yh), hzy)
69  +n3 = NM.n3b(1n, {==}, F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{yl, yh}), hea(yl, yh), hfr(yl, yh), FC.hF(yl, yh), hzy)
70  +nz = mpos_c(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh}), SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), n1, n3, Nat.is_eq(SF.mant(F.Bits{yl, yh}), 0n), {==})
71  Equal.sym(Nat, 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), SF.mant(F.Bits{yl, yh}), N.sub_add(SF.mant(F.Bits{yl, yh}), 1n, nzle(SF.mant(F.Bits{yl, yh}), nz)))