def zy

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64mulc.bend:78

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/lib/lemmas/proofs/nat_algebra.bend as NA

78def zy(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n) == True{} : Bool}) -> {F.zero(s) == SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())) : F.F64}:
79  +em = Equal.trans(Nat, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.mul(SF.mant(F.Bits{xl, xh}), 0n), 0n, Equal.cong(Nat, Nat, z => Nat.mul(SF.mant(F.Bits{xl, xh}), z), SF.mant(F.Bits{yl, yh}), 0n, mant0(yl, yh, hc, hb)), NA.mul_zero(SF.mant(F.Bits{xl, xh})))
80  Equal.trans(F.F64, F.zero(s), SF.zero(s), SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), zero_v(s), Equal.sym(F.F64, SF.round(s, Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), SF.zero(s), Equal.cong(Nat, F.F64, z => SF.round(s, z, Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh})), SF.zb())), Nat.mul(SF.mant(F.Bits{xl, xh}), SF.mant(F.Bits{yl, yh})), 0n, em)))