def top_c
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64addv.bend:103
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addv.bend as F64addv
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/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as AF
103def top_c(+xl: U32, +xh: U32, +yl: U32, +yh: U32, +a1: Bool, +ha1: {Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n) == a1 : Bool}, +a2: Bool, +ha2: {Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n) == a2 : Bool}) -> {F.add(F.Bits{xl, xh}, F.Bits{yl, yh}) == SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}) : F.F64}:
104 match a1 a2:
105 case False{} False{}:
106 +r = AF.afin(xl, xh, yl, yh, ltf(xl, xh, ha1), ltf(yl, yh, ha2))
107 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, ha1)
108 +s2 = Equal.cong(Bool, F.F64, t => spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), False{}, ha2)
109 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), s1, Equal.trans(F.F64, spec_g(False{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), s2, ff(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})))))
110 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), r, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), sp))
111 case True{} False{}:
112 +e1 = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, ha1)
113 +hy = ltf(yl, yh, ha2)
114 +i1 = add_g(xl, xh, yl, yh)
115 +i2 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh})))), SF.efield(F.Bits{xl, xh}), 2047n, e1)
116 +i3 = Equal.cong(Cmp, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), t), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), t)), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})), GT{}, NC.cmp_gt(2047n, SF.efield(F.Bits{yl, yh}), hy))
117 +i4 = pick_same(Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.not(X.is_zero(F.frac(F.Bits{xl, xh})))))
118 +i5 = Equal.cong(Bool, F.F64, t => F.nan_or(F.Bits{xl, xh}, Bool.not(t)), 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, {==}))
119 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1)
120 +s2 = Equal.cong(Bool, F.F64, t => spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), False{}, ha2)
121 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), s1, s2))
122 +im = Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), GT{}), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), GT{})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i3, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), GT{}), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), GT{})), F.nan_or(F.Bits{xl, xh}, Bool.not(X.is_zero(F.frac(F.Bits{xl, xh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i4, Equal.trans(F.F64, F.nan_or(F.Bits{xl, xh}, Bool.not(X.is_zero(F.frac(F.Bits{xl, xh})))), F.nan_or(F.Bits{xl, xh}, Bool.not(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i5, tf(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})))))))
123 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), im, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), False{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), sp))
124 case False{} True{}:
125 +e2 = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, ha2)
126 +hx = ltf(xl, xh, ha1)
127 +i1 = add_g(xl, xh, yl, yh)
128 +i2 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), t, Nat.cmp(SF.efield(F.Bits{xl, xh}), t))), SF.efield(F.Bits{yl, yh}), 2047n, e2)
129 +i3 = Equal.cong(Cmp, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, t), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, t)), Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n), LT{}, NC.cmp_lt(SF.efield(F.Bits{xl, xh}), 2047n, hx))
130 +i4 = pick_same(Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{yl, yh}, Bool.not(X.is_zero(F.frac(F.Bits{yl, yh})))))
131 +i5 = Equal.cong(Bool, F.F64, t => F.nan_or(F.Bits{yl, yh}, Bool.not(t)), 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, {==}))
132 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, ha1)
133 +s2 = Equal.cong(Bool, F.F64, t => spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2)
134 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), s1, s2))
135 +im = Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n))), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, Nat.cmp(SF.efield(F.Bits{xl, xh}), 2047n))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, LT{}), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, LT{})), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i3, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, LT{}), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), 2047n, LT{})), F.nan_or(F.Bits{yl, yh}, Bool.not(X.is_zero(F.frac(F.Bits{yl, yh})))), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i4, Equal.trans(F.F64, F.nan_or(F.Bits{yl, yh}, Bool.not(X.is_zero(F.frac(F.Bits{yl, yh})))), F.nan_or(F.Bits{yl, yh}, Bool.not(Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n))), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i5, ft(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})))))))
136 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), im, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(False{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), sp))
137 case True{} True{}:
138 +e1 = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, ha1)
139 +e2 = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, ha2)
140 +i1 = add_g(xl, xh, yl, yh)
141 +i2 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, SF.efield(F.Bits{yl, yh}), Nat.cmp(t, SF.efield(F.Bits{yl, yh})))), SF.efield(F.Bits{xl, xh}), 2047n, e1)
142 +i3 = Equal.cong(Nat, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, t, Nat.cmp(2047n, t)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, t, Nat.cmp(2047n, t))), SF.efield(F.Bits{yl, yh}), 2047n, e2)
143 +i4 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(t), Bool.not(X.is_zero(F.frac(F.Bits{yl, yh}))))), F.nan()), 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, {==}))
144 +i5 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.not(t))), F.nan()), 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, {==}))
145 +s1 = Equal.cong(Bool, F.F64, t => spec_g(t, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), True{}, ha1)
146 +s2 = Equal.cong(Bool, F.F64, t => spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), t, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), True{}, ha2)
147 +sp = Equal.trans(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_c(xl, xh, yl, yh), Equal.trans(F.F64, spec_g(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{yl, yh}), 2047n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(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), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), s1, s2))
148 +im = Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i2, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, SF.efield(F.Bits{yl, yh}), Nat.cmp(2047n, SF.efield(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, 2047n, Nat.cmp(2047n, 2047n)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, 2047n, Nat.cmp(2047n, 2047n))), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i3, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, 2047n, Nat.cmp(2047n, 2047n)), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), 2047n, 2047n, Nat.cmp(2047n, 2047n))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.not(X.is_zero(F.frac(F.Bits{yl, yh}))))), F.nan()), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i4, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.not(X.is_zero(F.frac(F.Bits{yl, yh}))))), F.nan()), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), F.nan_or(F.Bits{xl, xh}, Bool.or(Bool.not(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n)), Bool.not(Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n)))), F.nan()), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), i5, tt(Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})))))))
149 Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), im, Equal.sym(F.F64, SF.add(F.Bits{xl, xh}, F.Bits{yl, yh}), spec_g(True{}, Nat.is_eq(SF.frac(F.Bits{xl, xh}), 0n), True{}, Nat.is_eq(SF.frac(F.Bits{yl, yh}), 0n), SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), F.Bits{xl, xh}, F.Bits{yl, yh}, SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh})), sp))