def dfin

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

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
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/math/typed/f64cmp.bend as FC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as EX
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend as DV

73# the finite nonzero quotient
74def dfin(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hzx: {Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)) == False{} : Bool}, +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}, +hax: {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == True{} : Bool}, +hay: {Nat.is_lt(SF.efield(F.Bits{yl, yh}), 2047n) == True{} : Bool}) -> {F.div_n(s, 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})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))) == SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}:
75  +n1x = NM.n1(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfr(xl, xh), FC.hF(xl, xh), hzx)
76  +n1y = 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)
77  +n2x = NM.n2(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfr(xl, xh), FC.hF(xl, xh), hzx)
78  +n2y = NM.n2(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)
79  +a53 = NM.n3a(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfr(xl, xh), FC.hF(xl, xh), hzx)
80  +b53 = NM.n3a(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)
81  +a52 = NM.n3b(1n, {==}, F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.frac(F.Bits{xl, xh}), hea(xl, xh), hfr(xl, xh), FC.hF(xl, xh), hzx)
82  +b52 = 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)
83  +ey = yp_eq(yl, yh, hzy)
84  +hB = Equal.trans(Nat, SW.value(F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{yl, yh})), C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n)), n1y, Equal.cong(Nat, Nat, t => C.shift(NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), t), SF.mant(F.Bits{yl, yh}), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), ey))
85  +r = DV.dcore(1n, {==}, s, 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})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.mant(F.Bits{xl, xh}), Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), NM.sa(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), NM.sa(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), SF.xexp(F.Bits{xl, xh}), SF.xexp(F.Bits{yl, yh}), n1x, hB, a53, a52, b53, b52, n2x, n2y, EX.sa_le(F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh})), EX.sa_le(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), EX.xexp_ge(SF.efield(F.Bits{xl, xh})), xexp_le(SF.efield(F.Bits{yl, yh}), hay))
86  +sp = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, SF.mant(F.Bits{xl, xh})), z)), Nat.min(Nat.mod(C.shift(200n, SF.mant(F.Bits{xl, xh})), z), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), SF.zb()), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), SF.kq()), 1n))), SF.mant(F.Bits{yl, yh}), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n), ey)
87  Equal.trans(F.F64, F.div_n(s, 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})), F.norm_e(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh})), F.norm_f(F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}))), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n))), Nat.min(Nat.mod(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n)), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), 3000n), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), 200n), 1n))), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), r, Equal.sym(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n))), Nat.min(Nat.mod(C.shift(200n, SF.mant(F.Bits{xl, xh})), 1n+Nat.sub(SF.mant(F.Bits{yl, yh}), 1n)), 1n)), Nat.sub(Nat.add(SF.xexp(F.Bits{xl, xh}), 3000n), Nat.add(Nat.add(SF.xexp(F.Bits{yl, yh}), 200n), 1n))), sp))