def div_value

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

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

302def div_value(+x: F.F64, +y: F.F64) -> SF.Div.value(x, y):
303  match x y:
304    case F.Bits{+xl, +xh} F.Bits{+yl, +yh}:
305      +hs = Equal.trans(Bool, Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), Equal.cong(Bool, Bool, z => Bool.xor(z, F.signbit(F.Bits{yl, yh})), F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh})), Equal.cong(Bool, Bool, z => Bool.xor(SF.sign(F.Bits{xl, xh}), z), F.signbit(F.Bits{yl, yh}), SF.sign(F.Bits{yl, yh}), FB.signbit_value(F.Bits{yl, yh})))
306      +i1 = dsh1(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n))
307      +i2 = dswap(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), hs, F.div_n(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), 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}))), F.div_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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}))), Equal.cong(Bool, F.F64, z => F.div_n(z, 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}))), Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), hs), 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}), 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}), hea(xl, xh)), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 2047n), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), hea(yl, yh)), X.is_zero(F.frac(F.Bits{yl, yh})), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), FB.fz_g(yl, yh, 1048575, {==}), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), hea(yl, yh)))
308      +i3 = dcase(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, F.div_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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}, Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), 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), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), dkR_c(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.or(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)))), {==}), dkZ_c(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), xl, xh, yl, yh, Bool.or(Bool.or(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n)), Bool.or(Bool.not(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), Bool.and(Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)))), {==}))
309      Equal.trans(F.F64, F.div_cls(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), dimpl(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), F.div_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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})))), dspec(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})))), Equal.trans(F.F64, F.div_cls(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), F.exp_field(F.Bits{xl, xh}), F.frac(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), F.frac(F.Bits{yl, yh}), Nat.is_eq(F.exp_field(F.Bits{xl, xh}), 2047n)), dimpl(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), 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), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 2047n), X.is_zero(F.frac(F.Bits{yl, yh})), Nat.is_eq(F.exp_field(F.Bits{yl, yh}), 0n), F.div_n(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh})), 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})))), dimpl(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 0n), F.div_n(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh})), 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})))), i1, i2), i3)