proofs/math/typed/f64divc.bend

bend-collections-laws-math@1.0.0.0 · 309 lines · 27 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
3import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
4import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
5import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
6import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
7import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
8import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
9import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
13import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64cmp.bend as FC
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64norm.bend as NM
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64mexp.bend as EX
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64divv.bend as DV
20
21# Div.value of spec/math/f64.bend: SoftFloat's f64_div (NaN, infinity and
22# zero cases, then the quotient of the normalized significands) is the
23# spec's div, IEEE 754-2019 §6.2/§7.3 around the exact-then-round quotient.
24
25def v(+x: U32) -> Nat:
26  U32.to_nat(x)
27
28def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}:
29  FL.hea(xl, xh)
30
31def fval_g(+xl: U32, +xh: U32, +m: U32, +hm: {m == U32{WD.mask(32n, 20n)} : U32}) -> {SW.value(WU.U64{xl, U32.and(xh, m)}) == SF.frac(F.Bits{xl, xh}) : Nat}:
32  FL.fval_g(xl, xh, m, hm)
33
34def hfr(+xl: U32, +xh: U32) -> {SW.value(F.frac(F.Bits{xl, xh})) == SF.frac(F.Bits{xl, xh}) : Nat}:
35  FL.hfr(xl, xh)
36
37def ltf(+xl: U32, +xh: U32, +h: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == False{} : Bool}) -> {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == True{} : Bool}:
38  Equal.trans(Bool, Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n), Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n)), True{}, FB.lt_ne(SF.efield(F.Bits{xl, xh}), 2047n, WW.low_lt(11n, C.high(20n, v(xh)))), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, h))
39
40def xl_c(+E: Nat, +h: {Nat.is_lt(E, 2047n) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(E, 0n) == c : Bool}) -> {Nat.is_le(SF.pick(Nat, c, Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 3971n) == True{} : Bool}:
41  match c:
42    case True{}:
43      {==}
44    case False{}:
45      L.subst(Nat, z => {Nat.is_le(z, 3971n) == True{} : Bool}, Nat.add(1925n, E), Nat.sub(Nat.add(E, SF.zb()), 1075n), Equal.sym(Nat, Nat.sub(Nat.add(E, SF.zb()), 1075n), Nat.add(1925n, E), FC.esub(E)), N.le_add_left(E, 2046n, 1925n, N.lt_succ_le(E, 2046n, h)))
46
47def xexp_le(+E: Nat, +h: {Nat.is_lt(E, 2047n) == True{} : Bool}) -> {Nat.is_le(SF.pick(Nat, Nat.is_eq(E, 0n), Nat.sub(SF.zb(), 1074n), Nat.sub(Nat.add(E, SF.zb()), 1075n)), 3971n) == True{} : Bool}:
48  xl_c(E, h, Nat.is_eq(E, 0n), {==})
49
50def nzle(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
51  match n:
52    case 0n:
53      NC.absurd_tf({Nat.is_le(1n, 0n) == True{} : Bool}, Equal.sym(Bool, True{}, False{}, hz))
54    case 1n+ +np:
55      N.zero_le(np)
56
57# a nonzero finite significand is positive
58def mpos_c(+sy: Nat, +m: Nat, +w: Nat, +hw: {w == C.shift(sy, m) : Nat}, +h52: {C.fits(52n, w) == False{} : Bool}, +z: Bool, +hz: {Nat.is_eq(m, 0n) == z : Bool}) -> {z == False{} : Bool}:
59  match z:
60    case True{}:
61      +e0 = N.eq_from_is_eq(m, 0n, hz)
62      +ew = Equal.trans(Nat, w, C.shift(sy, m), 0n, hw, Equal.trans(Nat, C.shift(sy, m), C.shift(sy, 0n), 0n, Equal.cong(Nat, Nat, t => C.shift(sy, t), m, 0n, e0), WW.shift_zero(sy)))
63      Equal.trans(Bool, True{}, C.fits(52n, w), False{}, Equal.cong(Nat, Bool, t => C.fits(52n, t), 0n, w, Equal.sym(Nat, w, 0n, ew)), h52)
64    case False{}:
65      {==}
66
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)))
72
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))
88
89def mant0(+xl: U32, +xh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == True{} : Bool}) -> {SF.mant(F.Bits{xl, xh}) == 0n : Nat}:
90  +e1 = Equal.cong(Bool, Nat, t => Nat.add(SF.frac(F.Bits{xl, xh}), C.shift(52n, SF.b2n(Bool.not(t)))), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), True{}, hc)
91  Equal.trans(Nat, SF.mant(F.Bits{xl, xh}), Nat.add(SF.frac(F.Bits{xl, xh}), 0n), 0n, e1, Equal.trans(Nat, Nat.add(SF.frac(F.Bits{xl, xh}), 0n), SF.frac(F.Bits{xl, xh}), 0n, N.add_zero(SF.frac(F.Bits{xl, xh})), N.eq_from_is_eq(SF.frac(F.Bits{xl, xh}), 0n, hb)))
92
93def zero_v(+s: Bool) -> {F.zero(s) == SF.zero(s) : F.F64}:
94  match s:
95    case True{}:
96      {==}
97    case False{}:
98      {==}
99
100# zero divided by a nonzero finite double
101def dz(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +hc: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n) == True{} : Bool}, +hb: {Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n) == True{} : 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}) -> {F.zero(s) == SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}:
102  +e1 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, z), SF.mant(F.Bits{yl, yh}))), Nat.min(Nat.mod(C.shift(200n, z), SF.mant(F.Bits{yl, yh})), 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{xl, xh}), 0n, mant0(xl, xh, hc, hb))
103  +e2 = Equal.cong(Nat, F.F64, z => SF.round(s, Nat.add(Nat.mul(2n, Nat.div(C.shift(200n, 0n), z)), Nat.min(Nat.mod(C.shift(200n, 0n), 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), yp_eq(yl, yh, hzy))
104  Equal.trans(F.F64, F.zero(s), SF.zero(s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), zero_v(s), Equal.sym(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.zero(s), Equal.trans(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, 0n), SF.mant(F.Bits{yl, yh}))), Nat.min(Nat.mod(C.shift(200n, 0n), SF.mant(F.Bits{yl, yh})), 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.zero(s), e1, e2)))
105
106def dimpl(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64:
107  SF.pick(F.F64, a1, SF.pick(F.F64, Bool.or(Bool.not(b1), a2), F.nan(), F.inf(s)), SF.pick(F.F64, a2, SF.pick(F.F64, Bool.not(b2), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(c2, b2), SF.pick(F.F64, Bool.and(c1, b1), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(c1, b1), F.zero(s), r))))
108
109def dspec(+s: Bool, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +r: F.F64) -> F.F64:
110  SF.pick(F.F64, Bool.or(Bool.and(a1, Bool.not(b1)), Bool.and(a2, Bool.not(b2))), SF.qnan(), SF.pick(F.F64, Bool.and(a1, b1), SF.pick(F.F64, Bool.and(a2, b2), SF.qnan(), SF.inf(s)), SF.pick(F.F64, Bool.and(a2, b2), SF.zero(s), SF.pick(F.F64, Bool.and(c2, b2), SF.pick(F.F64, Bool.and(c1, b1), SF.qnan(), SF.inf(s)), r))))
111
112def ion(+s: Bool, +b: Bool) -> {F.inf_or_nan(s, b) == SF.pick(F.F64, b, F.nan(), F.inf(s)) : F.F64}:
113  match b:
114    case True{}:
115      Equal.trans(F.F64, F.inf_or_nan(s, True{}), F.nan(), SF.pick(F.F64, True{}, F.nan(), F.inf(s)), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.nan(), F.inf(s)), F.nan(), FR.pk_t(F.F64, F.nan(), F.inf(s))))
116    case False{}:
117      Equal.trans(F.F64, F.inf_or_nan(s, False{}), F.inf(s), SF.pick(F.F64, False{}, F.nan(), F.inf(s)), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.nan(), F.inf(s)), F.inf(s), FR.pk_f(F.F64, F.nan(), F.inf(s))))
118
119def non(+x: F.F64, +b: Bool) -> {F.nan_or(x, b) == SF.pick(F.F64, b, F.nan(), x) : F.F64}:
120  FL.non(x, b)
121
122def dsh4(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +z: Bool) -> {F.div_za(s, ea, fa, eb, fb, z) == SF.pick(F.F64, z, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))) : F.F64}:
123  match z:
124    case True{}:
125      Equal.trans(F.F64, F.div_za(s, ea, fa, eb, fb, True{}), F.zero(s), SF.pick(F.F64, True{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), F.zero(s), FR.pk_t(F.F64, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))
126    case False{}:
127      Equal.trans(F.F64, F.div_za(s, ea, fa, eb, fb, False{}), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)), SF.pick(F.F64, False{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)), FR.pk_f(F.F64, F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))
128
129def dsh3(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +z: Bool) -> {F.div_z(s, ea, fa, eb, fb, z) == SF.pick(F.F64, z, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))) : F.F64}:
130  match z:
131    case True{}:
132      Equal.trans(F.F64, F.div_z(s, ea, fa, eb, fb, True{}), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), ion(s, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), FR.pk_t(F.F64, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))))
133    case False{}:
134      Equal.trans(F.F64, F.div_z(s, ea, fa, eb, fb, False{}), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), dsh4(s, ea, fa, eb, fb, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa))), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))), FR.pk_f(F.F64, SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))))
135
136def dsh2(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +t: Bool) -> {F.div_b(s, ea, fa, eb, fb, t) == SF.pick(F.F64, t, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))) : F.F64}:
137  match t:
138    case True{}:
139      Equal.trans(F.F64, F.div_b(s, ea, fa, eb, fb, True{}), SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), non(F.zero(s), Bool.not(X.is_zero(fb))), Equal.sym(F.F64, SF.pick(F.F64, True{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), FR.pk_t(F.F64, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))))
140    case False{}:
141      Equal.trans(F.F64, F.div_b(s, ea, fa, eb, fb, False{}), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), dsh3(s, ea, fa, eb, fb, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb))), Equal.sym(F.F64, SF.pick(F.F64, False{}, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))))), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))), FR.pk_f(F.F64, SF.pick(F.F64, Bool.not(X.is_zero(fb)), F.nan(), F.zero(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(eb, 0n), X.is_zero(fb)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.nan(), F.inf(s)), SF.pick(F.F64, Bool.and(Nat.is_eq(ea, 0n), X.is_zero(fa)), F.zero(s), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb)))))))
142
143def dsh1(+s: Bool, +ea: Nat, +fa: WU.U64, +eb: Nat, +fb: WU.U64, +t: Bool) -> {F.div_cls(s, ea, fa, eb, fb, t) == dimpl(s, t, X.is_zero(fa), Nat.is_eq(ea, 0n), Nat.is_eq(eb, 2047n), X.is_zero(fb), Nat.is_eq(eb, 0n), F.div_n(s, F.norm_e(ea, fa), F.norm_f(ea, fa), F.norm_e(eb, fb), F.norm_f(eb, fb))) : F.F64}:
144  match t:
145    case True{}:
146      ion(s, Bool.or(Bool.not(X.is_zero(fa)), Nat.is_eq(eb, 2047n)))
147    case False{}:
148      dsh2(s, ea, fa, eb, fb, Nat.is_eq(eb, 2047n))
149
150def dcase(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +r1: F.F64, +r2: F.F64, +a1: Bool, +b1: Bool, +c1: Bool, +a2: Bool, +b2: Bool, +c2: Bool, +hR: {SF.pick(F.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.and(c1, b1), Bool.and(c2, b2))), r2, r1) == r2 : F.F64}, +hZ: {SF.pick(F.F64, Bool.or(Bool.or(a1, a2), Bool.or(Bool.not(Bool.and(c1, b1)), Bool.and(c2, b2))), r2, F.zero(s)) == r2 : F.F64}) -> {dimpl(s, a1, b1, c1, a2, b2, c2, r1) == dspec(s, a1, b1, c1, a2, b2, c2, r2) : F.F64}:
151  match a1 b1 c1 a2 b2 c2:
152    case True{} True{} True{} True{} True{} True{}:
153      {==}
154    case True{} True{} True{} True{} True{} False{}:
155      {==}
156    case True{} True{} True{} True{} False{} True{}:
157      {==}
158    case True{} True{} True{} True{} False{} False{}:
159      {==}
160    case True{} True{} True{} False{} True{} True{}:
161      FR.inf_v(s)
162    case True{} True{} True{} False{} True{} False{}:
163      FR.inf_v(s)
164    case True{} True{} True{} False{} False{} True{}:
165      FR.inf_v(s)
166    case True{} True{} True{} False{} False{} False{}:
167      FR.inf_v(s)
168    case True{} True{} False{} True{} True{} True{}:
169      {==}
170    case True{} True{} False{} True{} True{} False{}:
171      {==}
172    case True{} True{} False{} True{} False{} True{}:
173      {==}
174    case True{} True{} False{} True{} False{} False{}:
175      {==}
176    case True{} True{} False{} False{} True{} True{}:
177      FR.inf_v(s)
178    case True{} True{} False{} False{} True{} False{}:
179      FR.inf_v(s)
180    case True{} True{} False{} False{} False{} True{}:
181      FR.inf_v(s)
182    case True{} True{} False{} False{} False{} False{}:
183      FR.inf_v(s)
184    case True{} False{} True{} True{} True{} True{}:
185      {==}
186    case True{} False{} True{} True{} True{} False{}:
187      {==}
188    case True{} False{} True{} True{} False{} True{}:
189      {==}
190    case True{} False{} True{} True{} False{} False{}:
191      {==}
192    case True{} False{} True{} False{} True{} True{}:
193      {==}
194    case True{} False{} True{} False{} True{} False{}:
195      {==}
196    case True{} False{} True{} False{} False{} True{}:
197      {==}
198    case True{} False{} True{} False{} False{} False{}:
199      {==}
200    case True{} False{} False{} True{} True{} True{}:
201      {==}
202    case True{} False{} False{} True{} True{} False{}:
203      {==}
204    case True{} False{} False{} True{} False{} True{}:
205      {==}
206    case True{} False{} False{} True{} False{} False{}:
207      {==}
208    case True{} False{} False{} False{} True{} True{}:
209      {==}
210    case True{} False{} False{} False{} True{} False{}:
211      {==}
212    case True{} False{} False{} False{} False{} True{}:
213      {==}
214    case True{} False{} False{} False{} False{} False{}:
215      {==}
216    case False{} True{} True{} True{} True{} True{}:
217      zero_v(s)
218    case False{} True{} True{} True{} True{} False{}:
219      zero_v(s)
220    case False{} True{} True{} True{} False{} True{}:
221      {==}
222    case False{} True{} True{} True{} False{} False{}:
223      {==}
224    case False{} True{} True{} False{} True{} True{}:
225      {==}
226    case False{} True{} True{} False{} True{} False{}:
227      hZ
228    case False{} True{} True{} False{} False{} True{}:
229      hZ
230    case False{} True{} True{} False{} False{} False{}:
231      hZ
232    case False{} True{} False{} True{} True{} True{}:
233      zero_v(s)
234    case False{} True{} False{} True{} True{} False{}:
235      zero_v(s)
236    case False{} True{} False{} True{} False{} True{}:
237      {==}
238    case False{} True{} False{} True{} False{} False{}:
239      {==}
240    case False{} True{} False{} False{} True{} True{}:
241      FR.inf_v(s)
242    case False{} True{} False{} False{} True{} False{}:
243      hR
244    case False{} True{} False{} False{} False{} True{}:
245      hR
246    case False{} True{} False{} False{} False{} False{}:
247      hR
248    case False{} False{} True{} True{} True{} True{}:
249      zero_v(s)
250    case False{} False{} True{} True{} True{} False{}:
251      zero_v(s)
252    case False{} False{} True{} True{} False{} True{}:
253      {==}
254    case False{} False{} True{} True{} False{} False{}:
255      {==}
256    case False{} False{} True{} False{} True{} True{}:
257      FR.inf_v(s)
258    case False{} False{} True{} False{} True{} False{}:
259      hR
260    case False{} False{} True{} False{} False{} True{}:
261      hR
262    case False{} False{} True{} False{} False{} False{}:
263      hR
264    case False{} False{} False{} True{} True{} True{}:
265      zero_v(s)
266    case False{} False{} False{} True{} True{} False{}:
267      zero_v(s)
268    case False{} False{} False{} True{} False{} True{}:
269      {==}
270    case False{} False{} False{} True{} False{} False{}:
271      {==}
272    case False{} False{} False{} False{} True{} True{}:
273      FR.inf_v(s)
274    case False{} False{} False{} False{} True{} False{}:
275      hR
276    case False{} False{} False{} False{} False{} True{}:
277      hR
278    case False{} False{} False{} False{} False{} False{}:
279      hR
280
281def dswap(+s1: Bool, +s2: Bool, +hs: {s1 == s2 : Bool}, +r1: F.F64, +r2: F.F64, +hr: {r1 == r2 : F.F64}, +p1: Bool, +q1: Bool, +h0: {p1 == q1 : Bool}, +p2: Bool, +q2: Bool, +h1: {p2 == q2 : Bool}, +p3: Bool, +q3: Bool, +h2: {p3 == q3 : Bool}, +p4: Bool, +q4: Bool, +h3: {p4 == q4 : Bool}, +p5: Bool, +q5: Bool, +h4: {p5 == q5 : Bool}, +p6: Bool, +q6: Bool, +h5: {p6 == q6 : Bool}) -> {dimpl(s1, p1, p2, p3, p4, p5, p6, r1) == dimpl(s2, q1, q2, q3, q4, q5, q6, r2) : F.F64}:
282  Equal.trans(F.F64, dimpl(s1, p1, p2, p3, p4, p5, p6, r1), dimpl(s2, p1, p2, p3, p4, p5, p6, r1), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(w, p1, p2, p3, p4, p5, p6, r1), s1, s2, hs), Equal.trans(F.F64, dimpl(s2, p1, p2, p3, p4, p5, p6, r1), dimpl(s2, p1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(F.F64, F.F64, w => dimpl(s2, p1, p2, p3, p4, p5, p6, w), r1, r2, hr), Equal.trans(F.F64, dimpl(s2, p1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, w, p2, p3, p4, p5, p6, r2), p1, q1, h0), Equal.trans(F.F64, dimpl(s2, q1, p2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, w, p3, p4, p5, p6, r2), p2, q2, h1), Equal.trans(F.F64, dimpl(s2, q1, q2, p3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, w, p4, p5, p6, r2), p3, q3, h2), Equal.trans(F.F64, dimpl(s2, q1, q2, q3, p4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, q3, w, p5, p6, r2), p4, q4, h3), Equal.trans(F.F64, dimpl(s2, q1, q2, q3, q4, p5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, p6, r2), dimpl(s2, q1, q2, q3, q4, q5, q6, r2), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, q3, q4, w, p6, r2), p5, q5, h4), Equal.cong(Bool, F.F64, w => dimpl(s2, q1, q2, q3, q4, q5, w, r2), p6, q6, h5))))))))
283
284def dkR_c(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +g: Bool, +hg: {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)))) == g : Bool}) -> {SF.pick(F.F64, g, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), 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}:
285  match g:
286    case True{}:
287      Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), 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), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_t(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), 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})))), {==})
288    case False{}:
289      +ha = FC.or_l(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))), hg)
290      +hz = FC.or_r(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))), hg)
291      Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), 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})))), 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), FR.pk_f(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), 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})))), dfin(s, xl, xh, yl, yh, FC.or_l(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)), hz), FC.or_r(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)), hz), ltf(xl, xh, FC.or_l(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), ha)), ltf(yl, yh, FC.or_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), ha))))
292
293def dkZ_c(+s: Bool, +xl: U32, +xh: U32, +yl: U32, +yh: U32, +g: Bool, +hg: {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)))) == g : Bool}) -> {SF.pick(F.F64, g, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)) == SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s) : F.F64}:
294  match g:
295    case True{}:
296      Equal.trans(F.F64, SF.pick(F.F64, True{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_t(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), {==})
297    case False{}:
298      +hz = FC.or_r(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))), hg)
299      +h1 = FR.not_f(Bool.and(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), FC.or_l(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)), hz))
300      Equal.trans(F.F64, SF.pick(F.F64, False{}, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), F.zero(s), SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), FR.pk_f(F.F64, SF.div_fin(F.Bits{xl, xh}, F.Bits{yl, yh}, s), F.zero(s)), dz(s, xl, xh, yl, yh, FC.and_l(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), h1), FC.and_r(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), h1), FC.or_r(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)), hz)))
301
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)