proofs/math/typed/f64addf.bend

bend-collections-laws-math@1.0.0.0 · 239 lines · 24 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
4import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
5import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
6import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
7import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
8import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
9import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
10import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
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/u32laws.bend as LW
14import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
15import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
16import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
17import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64light.bend as FL
18import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
19import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addc.bend as AC
20import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adde.bend as AE
21import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG
22import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addh.bend as AH
23
24# The finite case of Add.value: SoftFloat's addF64 on two finite doubles is
25# the spec's add_fin, the exact sum or difference at the common scale
26# rounded once (Flocq's round_NE of the exact sum; SoftFloat's addMagsF64 and
27# subMagsF64 case split on the exponent order).
28
29def v(+x: U32) -> Nat:
30  U32.to_nat(x)
31
32def hea(+xl: U32, +xh: U32) -> {F.exp_field(F.Bits{xl, xh}) == SF.efield(F.Bits{xl, xh}) : Nat}:
33  FB.ef_g(1n, {==}, xh, 1048576, {==}, 2047, {==})
34
35def 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}:
36  Equal.cong(Nat, Nat, z => Nat.add(v(xl), C.shift(32n, z)), v(U32.and(xh, m)), C.low(20n, v(xh)), FB.andm(xh, 20n, m, hm))
37
38def hfr(+xl: U32, +xh: U32) -> {SW.value(F.frac(F.Bits{xl, xh})) == SF.frac(F.Bits{xl, xh}) : Nat}:
39  fval_g(xl, xh, 1048575, {==})
40
41def hF(+xl: U32, +xh: U32) -> {C.fits(52n, SF.frac(F.Bits{xl, xh})) == True{} : Bool}:
42  FL.hF(xl, xh)
43
44def ap(+x: F.F64, +y: F.F64, +same: Bool) -> {F.add_pick(x, y, same) == SF.pick(F.F64, same, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))) : F.F64}:
45  match same:
46    case True{}:
47      Equal.trans(F.F64, F.add_pick(x, y, True{}), F.add_mags(x, y, F.signbit(x)), SF.pick(F.F64, True{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), F.add_mags(x, y, F.signbit(x)), FR.pk_t(F.F64, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x)))))
48    case False{}:
49      Equal.trans(F.F64, F.add_pick(x, y, False{}), F.sub_mags(x, y, F.signbit(x)), SF.pick(F.F64, False{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), F.sub_mags(x, y, F.signbit(x)), FR.pk_f(F.F64, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x)))))
50
51def le_rw(+a: Nat, +a2: Nat, +ha: {a == a2 : Nat}, +b: Nat, +b2: Nat, +hb: {b == b2 : Nat}, +h: {Nat.is_le(a2, b2) == True{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
52  +h2 = L.subst(Nat, z => {Nat.is_le(z, b2) == True{} : Bool}, a2, a, Equal.sym(Nat, a, a2, ha), h)
53  L.subst(Nat, z => {Nat.is_le(a, z) == True{} : Bool}, b2, b, Equal.sym(Nat, b, b2, hb), h2)
54
55def nz_le(+n: Nat, +hz: {Nat.is_eq(n, 0n) == False{} : Bool}) -> {Nat.is_le(1n, n) == True{} : Bool}:
56  FL.nz_le(n, hz)
57
58def xe_le_c(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}, +z: Bool, +hz: {Nat.is_eq(a, 0n) == z : Bool}) -> {Nat.is_le(AG.xe(a), AG.xe(b)) == True{} : Bool}:
59  match z:
60    case True{}:
61      +hb = N.le_trans(1n, 1n+a, b, N.zero_le(a), N.lt_succ_le_succ(a, b, h))
62      +xb = AG.xe_n(b, AG.posz(b, hb))
63      le_rw(AG.xe(a), 1926n, AG.xe_z(a, hz), AG.xe(b), Nat.add(1925n, b), xb, N.le_add_left(1n, b, 1925n, hb))
64    case False{}:
65      +hb = N.le_trans(1n, 1n+a, b, N.zero_le(a), N.lt_succ_le_succ(a, b, h))
66      +xb = AG.xe_n(b, AG.posz(b, hb))
67      le_rw(AG.xe(a), Nat.add(1925n, a), AG.xe_n(a, hz), AG.xe(b), Nat.add(1925n, b), xb, N.le_add_left(a, b, 1925n, N.lt_le(a, b, h)))
68
69def xe_le(+a: Nat, +b: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_le(AG.xe(a), AG.xe(b)) == True{} : Bool}:
70  xe_le_c(a, b, h, Nat.is_eq(a, 0n), {==})
71
72def xem_c(+e: Nat, +z: Bool, +hz: {Nat.is_eq(e, 0n) == z : Bool}) -> {Nat.add(1926n, Nat.sub(e, 1n)) == AG.xe(e) : Nat}:
73  match z:
74    case True{}:
75      +e0 = N.eq_from_is_eq(e, 0n, hz)
76      L.subst(Nat, w => {Nat.add(1926n, Nat.sub(w, 1n)) == AG.xe(w) : Nat}, 0n, e, Equal.sym(Nat, e, 0n, e0), {==})
77    case False{}:
78      +e1 = Equal.cong(Nat, Nat, w => Nat.add(1925n, w), Nat.add(1n, Nat.sub(e, 1n)), e, N.sub_add(e, 1n, nz_le(e, hz)))
79      Equal.trans(Nat, Nat.add(1926n, Nat.sub(e, 1n)), Nat.add(1925n, e), AG.xe(e), e1, Equal.sym(Nat, AG.xe(e), Nat.add(1925n, e), AG.xe_n(e, hz)))
80
81def xem(+e: Nat) -> {Nat.add(1926n, Nat.sub(e, 1n)) == AG.xe(e) : Nat}:
82  xem_c(e, Nat.is_eq(e, 0n), {==})
83
84def hovm(+e: Nat, +h: {Nat.is_lt(e, 2047n) == True{} : Bool}) -> {Nat.is_lt(Nat.add(Nat.sub(e, 1n), 1n), 2047n) == True{} : Bool}:
85  match e:
86    case 0n:
87      {==}
88    case 1n+ +p:
89      +e1 = Equal.trans(Nat, Nat.add(Nat.sub(p, 0n), 1n), Nat.add(p, 1n), 1n+p, Equal.cong(Nat, Nat, z => Nat.add(z, 1n), Nat.sub(p, 0n), p, N.sub_zero(p)), Equal.trans(Nat, Nat.add(p, 1n), 1n+Nat.add(p, 0n), 1n+p, N.add_succ(p, 0n), N.succ_cong(Nat.add(p, 0n), p, N.add_zero(p))))
90      L.subst(Nat, z => {Nat.is_lt(z, 2047n) == True{} : Bool}, 1n+p, Nat.add(Nat.sub(p, 0n), 1n), Equal.sym(Nat, Nat.add(Nat.sub(p, 0n), 1n), 1n+p, e1), h)
91
92def rc2(+s: Bool, +s2: Bool, +hs: {s == s2 : Bool}, +m: Nat, +m2: Nat, +hm: {m == m2 : Nat}, +x: Nat, +x2: Nat, +hx: {x == x2 : Nat}) -> {SF.round(s, m, x) == SF.round(s2, m2, x2) : F.F64}:
93  +e1 = L.subst(Bool, z => {SF.round(s, m, x) == SF.round(z, m, x) : F.F64}, s, s2, hs, {==})
94  +e2 = L.subst(Nat, z => {SF.round(s, m, x) == SF.round(s2, z, x) : F.F64}, m, m2, hm, e1)
95  L.subst(Nat, z => {SF.round(s, m, x) == SF.round(s2, m2, z) : F.F64}, x, x2, hx, e2)
96
97def spec_lt(+sa: Bool, +sb: Bool, +ea: Nat, +eb: Nat, +Fa: Nat, +Fb: Nat, +h: {Nat.is_le(AG.xe(ea), AG.xe(eb)) == True{} : Bool}) -> {SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))) == SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)) : F.F64}:
98  +e1 = Equal.cong(Nat, F.F64, w => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), w), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), w), AG.mt(eb, Fb)), w), Nat.min(AG.xe(ea), AG.xe(eb)), AG.xe(ea), AG.min_l(AG.xe(ea), AG.xe(eb), h))
99  +e2 = Equal.cong(Nat, F.F64, z => SF.add_mag(sa, C.shift(z, AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), Nat.sub(AG.xe(ea), AG.xe(ea)), 0n, N.sub_self(AG.xe(ea)))
100  +e3 = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.add_mag(sa, C.shift(0n, AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), e2, Equal.cong(Nat, F.F64, zz_ => SF.add_mag(sa, zz_, sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), C.shift(0n, AG.mt(ea, Fa)), AG.mt(ea, Fa), {==}))
101  Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), e1, e3)
102
103def spec_gt(+sa: Bool, +sb: Bool, +ea: Nat, +eb: Nat, +Fa: Nat, +Fb: Nat, +h: {Nat.is_le(AG.xe(eb), AG.xe(ea)) == True{} : Bool}) -> {SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))) == SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)) : F.F64}:
104  +e1 = Equal.cong(Nat, F.F64, w => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), w), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), w), AG.mt(eb, Fb)), w), Nat.min(AG.xe(ea), AG.xe(eb)), AG.xe(eb), AG.min_r(AG.xe(ea), AG.xe(eb), h))
105  +e2 = Equal.cong(Nat, F.F64, z => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(z, AG.mt(eb, Fb)), AG.xe(eb)), Nat.sub(AG.xe(eb), AG.xe(eb)), 0n, N.sub_self(AG.xe(eb)))
106  +e3 = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(eb)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(0n, AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), e2, Equal.cong(Nat, F.F64, zz_ => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, zz_, AG.xe(eb)), C.shift(0n, AG.mt(eb, Fb)), AG.mt(eb, Fb), {==}))
107  Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(eb)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), e1, e3)
108
109def spec_eq(+sa: Bool, +sb: Bool, +ea: Nat, +Fa: Nat, +Fb: Nat) -> {SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fb)), Nat.min(AG.xe(ea), AG.xe(ea))) == SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)) : F.F64}:
110  +e1 = Equal.cong(Nat, F.F64, w => SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), w), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), w), AG.mt(ea, Fb)), w), Nat.min(AG.xe(ea), AG.xe(ea)), AG.xe(ea), AG.min_l(AG.xe(ea), AG.xe(ea), N.le_refl(AG.xe(ea))))
111  +e2 = Equal.cong(Nat, F.F64, z => SF.add_mag(sa, C.shift(z, AG.mt(ea, Fa)), sb, C.shift(z, AG.mt(ea, Fb)), AG.xe(ea)), Nat.sub(AG.xe(ea), AG.xe(ea)), 0n, N.sub_self(AG.xe(ea)))
112  +e3 = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, C.shift(0n, AG.mt(ea, Fa)), sb, C.shift(0n, AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), e2, Equal.cong(F.F64, F.F64, zz_ => zz_, SF.add_mag(sa, C.shift(0n, AG.mt(ea, Fa)), sb, C.shift(0n, AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), {==}))
113  Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fb)), Nat.min(AG.xe(ea), AG.xe(ea))), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), AG.xe(ea)), AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), e1, e3)
114
115def caseLT(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +ea: Nat, +eb: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +hb: {Nat.is_eq(eb, 2047n) == False{} : Bool}, +hlt: {Nat.is_lt(ea, eb) == True{} : Bool}, +sg: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == sg : Bool}) -> {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})) == SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)) : F.F64}:
116  match sg:
117    case True{}:
118      +i1 = Equal.cong(Bool, F.F64, t => F.am_big(y, sa, eb, F.frac(y), ea, F.frac(x), t), Nat.is_eq(eb, 2047n), False{}, hb)
119      +i2 = AH.bigA(one, h1, sa, eb, F.frac(y), ea, F.frac(x), Fb, Fa, hfb, hfa, hFb, hFa, hlt)
120      +sp = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))))), Bool.not(Bool.xor(sa, sb)), True{}, hsg)
121      Equal.trans(F.F64, SF.pick(F.F64, True{}, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), F.am_case(x, y, sa, ea, eb, LT{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), FR.pk_t(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), F.rp62(sa, Nat.add(F.off(), eb), X.add(X.add(WU.U64{0, 536870912}, X.shl(F.frac(y), 9n)), X.shr_jam(F.am_small(ea, X.shl(F.frac(x), 9n)), Nat.sub(eb, ea)))), SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), i1, i2), Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), sp)))
122    case False{}:
123      +i1 = Equal.cong(Bool, F.F64, t => F.sm_big(y, Bool.not(sa), eb, F.frac(y), ea, F.frac(x), t), Nat.is_eq(eb, 2047n), False{}, hb)
124      +i2 = AH.bigS(one, h1, Bool.not(sa), eb, F.frac(y), ea, F.frac(x), Fb, Fa, hfb, hfa, hFb, hFa, hlt)
125      +i3 = Equal.cong(Bool, F.F64, t => SF.round(t, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), Bool.not(sa), sb, AG.sgn(sa, sb, hsg))
126      +sp1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))))), Bool.not(Bool.xor(sa, sb)), False{}, hsg)
127      +sp2 = Equal.cong(Cmp, F.F64, t => SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), t), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb))), LT{}, AG.bigcmp(one, h1, eb, ea, Fb, Fa, hFb, hFa, hlt))
128      +imp = Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, LT{}), F.norm_round_pack(Bool.not(sa), Nat.add(F.off(), Nat.sub(eb, 1n)), X.sub(X.add(X.shl(F.frac(y), 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(ea, X.shl(F.frac(x), 10n)), Nat.sub(eb, ea)))), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), i1, Equal.trans(F.F64, F.norm_round_pack(Bool.not(sa), Nat.add(F.off(), Nat.sub(eb, 1n)), X.sub(X.add(X.shl(F.frac(y), 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(ea, X.shl(F.frac(x), 10n)), Nat.sub(eb, ea)))), SF.round(Bool.not(sa), Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), i2, i3))
129      +spc = Equal.trans(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)))), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), sp1, sp2)
130      Equal.trans(F.F64, SF.pick(F.F64, False{}, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), F.sm_case(x, y, sa, ea, eb, LT{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), FR.pk_f(F.F64, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, LT{}), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), imp, Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.round(sb, Nat.sub(C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.mt(ea, Fa)), AG.xe(ea)), spc)))
131
132def caseGT(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +ea: Nat, +eb: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +ha: {Nat.is_eq(ea, 2047n) == False{} : Bool}, +hgt: {Nat.is_lt(eb, ea) == True{} : Bool}, +sg: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == sg : Bool}) -> {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})) == SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)) : F.F64}:
133  match sg:
134    case True{}:
135      +i1 = Equal.cong(Bool, F.F64, t => F.am_big(x, sa, ea, F.frac(x), eb, F.frac(y), t), Nat.is_eq(ea, 2047n), False{}, ha)
136      +i2 = AH.bigA(one, h1, sa, ea, F.frac(x), eb, F.frac(y), Fa, Fb, hfa, hfb, hFa, hFb, hgt)
137      +i3 = Equal.cong(Nat, F.F64, z => SF.round(sa, z, AG.xe(eb)), Nat.add(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))), Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), NA.add_comm(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))))
138      +sp = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)))), Bool.not(Bool.xor(sa, sb)), True{}, hsg)
139      +imp = Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), F.rp62(sa, Nat.add(F.off(), ea), X.add(X.add(WU.U64{0, 536870912}, X.shl(F.frac(x), 9n)), X.shr_jam(F.am_small(eb, X.shl(F.frac(y), 9n)), Nat.sub(ea, eb)))), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), i1, Equal.trans(F.F64, F.rp62(sa, Nat.add(F.off(), ea), X.add(X.add(WU.U64{0, 536870912}, X.shl(F.frac(x), 9n)), X.shr_jam(F.am_small(eb, X.shl(F.frac(y), 9n)), Nat.sub(ea, eb)))), SF.round(sa, Nat.add(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))), AG.xe(eb)), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), i2, i3))
140      Equal.trans(F.F64, SF.pick(F.F64, True{}, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), F.am_case(x, y, sa, ea, eb, GT{}), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), FR.pk_t(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), Equal.trans(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), imp, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), sp)))
141    case False{}:
142      +i1 = Equal.cong(Bool, F.F64, t => F.sm_big(x, sa, ea, F.frac(x), eb, F.frac(y), t), Nat.is_eq(ea, 2047n), False{}, ha)
143      +i2 = AH.bigS(one, h1, sa, ea, F.frac(x), eb, F.frac(y), Fa, Fb, hfa, hfb, hFa, hFb, hgt)
144      +c1 = AG.bigcmp(one, h1, ea, eb, Fa, Fb, hFa, hFb, hgt)
145      +c2 = Equal.trans(Cmp, Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), SF.flip(Nat.cmp(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))), GT{}, Equal.sym(Cmp, SF.flip(Nat.cmp(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), NC.cmp_flip(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)))), Equal.cong(Cmp, Cmp, t => SF.flip(t), Nat.cmp(AG.mt(eb, Fb), C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa))), LT{}, c1))
146      +sp1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)))), Bool.not(Bool.xor(sa, sb)), False{}, hsg)
147      +sp2 = Equal.cong(Cmp, F.F64, t => SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), t), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), GT{}, c2)
148      +imp = Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, GT{}), F.norm_round_pack(sa, Nat.add(F.off(), Nat.sub(ea, 1n)), X.sub(X.add(X.shl(F.frac(x), 10n), WU.U64{0, 1073741824}), X.shr_jam(F.sm_small(eb, X.shl(F.frac(y), 10n)), Nat.sub(ea, eb)))), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), i1, i2)
149      +spc = Equal.trans(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.sub_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb), Nat.cmp(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb))), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), sp1, sp2)
150      Equal.trans(F.F64, SF.pick(F.F64, False{}, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), F.sm_case(x, y, sa, ea, eb, GT{}), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), FR.pk_f(F.F64, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), Equal.trans(F.F64, F.sm_case(x, y, sa, ea, eb, GT{}), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), imp, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.round(sa, Nat.sub(C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), AG.mt(eb, Fb)), AG.xe(eb)), spc)))
151
152def aeq_c(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +ea: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +ha: {Nat.is_eq(ea, 2047n) == False{} : Bool}, +z: Bool, +hz: {Nat.is_eq(ea, 0n) == z : Bool}) -> {F.am_eq(x, sa, ea, F.frac(x), F.frac(y)) == SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)) : F.F64}:
153  match z:
154    case True{}:
155      +e0 = N.eq_from_is_eq(ea, 0n, hz)
156      +r0 = AC.ame0(one, h1, sa, F.frac(x), F.frac(y), Fa, Fb, hfa, hfb, hFa, hFb)
157      +b0 = Equal.cong(Nat, F.F64, w => SF.round(sa, w, 1926n), Nat.add(Fa, Fb), Nat.add(Nat.add(Fa, 0n), Nat.add(Fb, 0n)), Equal.trans(Nat, Nat.add(Fa, Fb), Nat.add(Nat.add(Fa, 0n), Fb), Nat.add(Nat.add(Fa, 0n), Nat.add(Fb, 0n)), Equal.cong(Nat, Nat, w => Nat.add(w, Fb), Fa, Nat.add(Fa, 0n), Equal.sym(Nat, Nat.add(Fa, 0n), Fa, N.add_zero(Fa))), Equal.cong(Nat, Nat, w => Nat.add(Nat.add(Fa, 0n), w), Fb, Nat.add(Fb, 0n), Equal.sym(Nat, Nat.add(Fb, 0n), Fb, N.add_zero(Fb)))))
158      +p0 = Equal.trans(F.F64, F.am_eq(x, sa, 0n, F.frac(x), F.frac(y)), SF.round(sa, Nat.add(Fa, Fb), 1926n), SF.round(sa, Nat.add(AG.mt(0n, Fa), AG.mt(0n, Fb)), AG.xe(0n)), r0, b0)
159      L.subst(Nat, w => {F.am_eq(x, sa, w, F.frac(x), F.frac(y)) == SF.round(sa, Nat.add(AG.mt(w, Fa), AG.mt(w, Fb)), AG.xe(w)) : F.F64}, 0n, ea, Equal.sym(Nat, ea, 0n, e0), p0)
160    case False{}:
161      +ep = AG.pred_eq(ea, hz)
162      +hp = L.subst(Nat, w => {Nat.is_eq(w, 2047n) == False{} : Bool}, ea, 1n+N.pred(ea), Equal.sym(Nat, 1n+N.pred(ea), ea, ep), ha)
163      +i1 = Equal.cong(Bool, F.F64, t => F.am_eq_n(x, sa, 1n+N.pred(ea), F.frac(x), F.frac(y), t), Nat.is_eq(1n+N.pred(ea), 2047n), False{}, hp)
164      +i2 = AC.amen(one, h1, sa, 1n+N.pred(ea), F.frac(x), F.frac(y), Fa, Fb, hfa, hfb, hFa, hFb, 2097152, {==})
165      +q1 = Equal.trans(F.F64, F.am_eq(x, sa, 1n+N.pred(ea), F.frac(x), F.frac(y)), F.round_pack(sa, Nat.add(F.off(), 1n+N.pred(ea)), X.shl(X.add(WU.U64{0, 2097152}, X.add(F.frac(x), F.frac(y))), 9n)), SF.round(sa, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, 1n+N.pred(ea))), i1, i2)
166      +q = L.subst(Nat, w => {F.am_eq(x, sa, w, F.frac(x), F.frac(y)) == SF.round(sa, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, w)) : F.F64}, 1n+N.pred(ea), ea, ep, q1)
167      +ma = AG.mt_n(one, h1, ea, Fa, hz)
168      +mb = AG.mt_n(one, h1, ea, Fb, hz)
169      +em = Equal.trans(Nat, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(AG.mt(ea, Fa), Nat.add(Fb, C.shift(52n, one))), Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), Equal.cong(Nat, Nat, w => Nat.add(w, Nat.add(Fb, C.shift(52n, one))), Nat.add(Fa, C.shift(52n, one)), AG.mt(ea, Fa), Equal.sym(Nat, AG.mt(ea, Fa), Nat.add(Fa, C.shift(52n, one)), ma)), Equal.cong(Nat, Nat, w => Nat.add(AG.mt(ea, Fa), w), Nat.add(Fb, C.shift(52n, one)), AG.mt(ea, Fb), Equal.sym(Nat, AG.mt(ea, Fb), Nat.add(Fb, C.shift(52n, one)), mb)))
170      +b = rc2(sa, sa, {==}, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), em, Nat.add(1925n, ea), AG.xe(ea), Equal.sym(Nat, AG.xe(ea), Nat.add(1925n, ea), AG.xe_n(ea, hz)))
171      Equal.trans(F.F64, F.am_eq(x, sa, ea, F.frac(x), F.frac(y)), SF.round(sa, Nat.add(Nat.add(Fa, C.shift(52n, one)), Nat.add(Fb, C.shift(52n, one))), Nat.add(1925n, ea)), SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), q, b)
172
173def seq(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == False{} : Bool}, +ea: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +hlta: {Nat.is_lt(ea, 2047n) == True{} : Bool}, +d: Cmp, +hd: {Nat.cmp(Fa, Fb) == d : Cmp}) -> {F.sm_eq2(sa, ea, F.frac(x), F.frac(y), d) == SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), d) : F.F64}:
174  match d:
175    case EQ{}:
176      AG.zero_v(False{})
177    case GT{}:
178      +hlt = NC.lt_of_gt(Fa, Fb, hd)
179      +hle = L.subst(Nat, w => {Nat.is_le(w, SW.value(F.frac(x))) == True{} : Bool}, Fb, SW.value(F.frac(y)), Equal.sym(Nat, SW.value(F.frac(y)), Fb, hfb), L.subst(Nat, w => {Nat.is_le(Fb, w) == True{} : Bool}, Fa, SW.value(F.frac(x)), Equal.sym(Nat, SW.value(F.frac(x)), Fa, hfa), N.lt_le(Fb, Fa, hlt)))
180      +hdv = Equal.trans(Nat, SW.value(X.sub(F.frac(x), F.frac(y))), Nat.sub(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.sub(Fa, Fb), WA.sub_value(F.frac(x), F.frac(y), hle), Equal.trans(Nat, Nat.sub(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.sub(Fa, SW.value(F.frac(y))), Nat.sub(Fa, Fb), Equal.cong(Nat, Nat, w => Nat.sub(w, SW.value(F.frac(y))), SW.value(F.frac(x)), Fa, hfa), Equal.cong(Nat, Nat, w => Nat.sub(Fa, w), SW.value(F.frac(y)), Fb, hfb)))
181      +hD = Equal.trans(Bool, C.fits(52n, Nat.sub(Fa, Fb)), Nat.is_lt(Nat.sub(Fa, Fb), C.shift(52n, one)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.sub(Fa, Fb), C.shift(52n, one)), C.fits(52n, Nat.sub(Fa, Fb)), FR.lt_fit(52n, one, h1, Nat.sub(Fa, Fb))), N.le_lt_trans(Nat.sub(Fa, Fb), Fa, C.shift(52n, one), AG.sub_le(Fa, Fb), Equal.trans(Bool, Nat.is_lt(Fa, C.shift(52n, one)), C.fits(52n, Fa), True{}, FR.lt_fit(52n, one, h1, Fa), hFa)))
182      +hz = AG.posz(Nat.sub(Fa, Fb), FR.lt_sub_pos(Fb, Fa, hlt))
183      +r = AE.smx(one, h1, sa, Nat.sub(ea, 1n), X.sub(F.frac(x), F.frac(y)), Nat.sub(Fa, Fb), hdv, hD, hz, hovm(ea, hlta))
184      +b = rc2(sa, sa, {==}, Nat.sub(Fa, Fb), Nat.sub(AG.mt(ea, Fa), AG.mt(ea, Fb)), Equal.sym(Nat, Nat.sub(AG.mt(ea, Fa), AG.mt(ea, Fb)), Nat.sub(Fa, Fb), FR.sub_cancel_r(Fa, Fb, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(ea, 0n)))))), Nat.add(1926n, Nat.sub(ea, 1n)), AG.xe(ea), xem(ea))
185      Equal.trans(F.F64, F.sm_exact(sa, Nat.sub(ea, 1n), X.sub(F.frac(x), F.frac(y))), SF.round(sa, Nat.sub(Fa, Fb), Nat.add(1926n, Nat.sub(ea, 1n))), SF.round(sa, Nat.sub(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), r, b)
186    case LT{}:
187      +hlt = NC.lt_of_cmp(Fa, Fb, hd)
188      +hle = L.subst(Nat, w => {Nat.is_le(w, SW.value(F.frac(y))) == True{} : Bool}, Fa, SW.value(F.frac(x)), Equal.sym(Nat, SW.value(F.frac(x)), Fa, hfa), L.subst(Nat, w => {Nat.is_le(Fa, w) == True{} : Bool}, Fb, SW.value(F.frac(y)), Equal.sym(Nat, SW.value(F.frac(y)), Fb, hfb), N.lt_le(Fa, Fb, hlt)))
189      +hdv = Equal.trans(Nat, SW.value(X.sub(F.frac(y), F.frac(x))), Nat.sub(SW.value(F.frac(y)), SW.value(F.frac(x))), Nat.sub(Fb, Fa), WA.sub_value(F.frac(y), F.frac(x), hle), Equal.trans(Nat, Nat.sub(SW.value(F.frac(y)), SW.value(F.frac(x))), Nat.sub(Fb, SW.value(F.frac(x))), Nat.sub(Fb, Fa), Equal.cong(Nat, Nat, w => Nat.sub(w, SW.value(F.frac(x))), SW.value(F.frac(y)), Fb, hfb), Equal.cong(Nat, Nat, w => Nat.sub(Fb, w), SW.value(F.frac(x)), Fa, hfa)))
190      +hD = Equal.trans(Bool, C.fits(52n, Nat.sub(Fb, Fa)), Nat.is_lt(Nat.sub(Fb, Fa), C.shift(52n, one)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.sub(Fb, Fa), C.shift(52n, one)), C.fits(52n, Nat.sub(Fb, Fa)), FR.lt_fit(52n, one, h1, Nat.sub(Fb, Fa))), N.le_lt_trans(Nat.sub(Fb, Fa), Fb, C.shift(52n, one), AG.sub_le(Fb, Fa), Equal.trans(Bool, Nat.is_lt(Fb, C.shift(52n, one)), C.fits(52n, Fb), True{}, FR.lt_fit(52n, one, h1, Fb), hFb)))
191      +hz = AG.posz(Nat.sub(Fb, Fa), FR.lt_sub_pos(Fa, Fb, hlt))
192      +r = AE.smx(one, h1, Bool.not(sa), Nat.sub(ea, 1n), X.sub(F.frac(y), F.frac(x)), Nat.sub(Fb, Fa), hdv, hD, hz, hovm(ea, hlta))
193      +b = rc2(Bool.not(sa), sb, AG.sgn(sa, sb, hsg), Nat.sub(Fb, Fa), Nat.sub(AG.mt(ea, Fb), AG.mt(ea, Fa)), Equal.sym(Nat, Nat.sub(AG.mt(ea, Fb), AG.mt(ea, Fa)), Nat.sub(Fb, Fa), FR.sub_cancel_r(Fb, Fa, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(ea, 0n)))))), Nat.add(1926n, Nat.sub(ea, 1n)), AG.xe(ea), xem(ea))
194      Equal.trans(F.F64, F.sm_exact(Bool.not(sa), Nat.sub(ea, 1n), X.sub(F.frac(y), F.frac(x))), SF.round(Bool.not(sa), Nat.sub(Fb, Fa), Nat.add(1926n, Nat.sub(ea, 1n))), SF.round(sb, Nat.sub(AG.mt(ea, Fb), AG.mt(ea, Fa)), AG.xe(ea)), r, b)
195
196def caseEQ(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +ea: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +hlta: {Nat.is_lt(ea, 2047n) == True{} : Bool}, +sg: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == sg : Bool}) -> {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})) == SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)) : F.F64}:
197  match sg:
198    case True{}:
199      +ha = N.is_eq_lt(ea, 2047n, hlta)
200      +i1 = aeq_c(one, h1, x, y, sa, ea, Fa, Fb, hfa, hfb, hFa, hFb, ha, Nat.is_eq(ea, 0n), {==})
201      +sp = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb)))), Bool.not(Bool.xor(sa, sb)), True{}, hsg)
202      Equal.trans(F.F64, SF.pick(F.F64, True{}, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), F.am_case(x, y, sa, ea, ea, EQ{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), FR.pk_t(F.F64, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), Equal.trans(F.F64, F.am_case(x, y, sa, ea, ea, EQ{}), SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), i1, Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), sp)))
203    case False{}:
204      +ha = N.is_eq_lt(ea, 2047n, hlta)
205      +i1 = Equal.cong(Bool, F.F64, t => F.sm_eq(sa, ea, F.frac(x), F.frac(y), t), Nat.is_eq(ea, 2047n), False{}, ha)
206      +ec = Equal.trans(Cmp, X.cmp(F.frac(x), F.frac(y)), Nat.cmp(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.cmp(Fa, Fb), AC.cmpv(F.frac(x), F.frac(y)), Equal.trans(Cmp, Nat.cmp(SW.value(F.frac(x)), SW.value(F.frac(y))), Nat.cmp(Fa, SW.value(F.frac(y))), Nat.cmp(Fa, Fb), Equal.cong(Nat, Cmp, w => Nat.cmp(w, SW.value(F.frac(y))), SW.value(F.frac(x)), Fa, hfa), Equal.cong(Nat, Cmp, w => Nat.cmp(Fa, w), SW.value(F.frac(y)), Fb, hfb)))
207      +i2 = Equal.cong(Cmp, F.F64, t => F.sm_eq2(sa, ea, F.frac(x), F.frac(y), t), X.cmp(F.frac(x), F.frac(y)), Nat.cmp(Fa, Fb), ec)
208      +i3 = seq(one, h1, x, y, sa, sb, hsg, ea, Fa, Fb, hfa, hfb, hFa, hFb, hlta, Nat.cmp(Fa, Fb), {==})
209      +sp1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, t, SF.round(sa, Nat.add(AG.mt(ea, Fa), AG.mt(ea, Fb)), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb)))), Bool.not(Bool.xor(sa, sb)), False{}, hsg)
210      +sp2 = Equal.cong(Cmp, F.F64, t => SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), t), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb)), Nat.cmp(Fa, Fb), NC.cmp_addr(Fa, Fb, C.shift(52n, SF.b2n(Bool.not(Nat.is_eq(ea, 0n))))))
211      +imp = Equal.trans(F.F64, F.sm_case(x, y, sa, ea, ea, EQ{}), F.sm_eq2(sa, ea, F.frac(x), F.frac(y), X.cmp(F.frac(x), F.frac(y))), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), i1, Equal.trans(F.F64, F.sm_eq2(sa, ea, F.frac(x), F.frac(y), X.cmp(F.frac(x), F.frac(y))), F.sm_eq2(sa, ea, F.frac(x), F.frac(y), Nat.cmp(Fa, Fb)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), i2, i3))
212      +spc = Equal.trans(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(AG.mt(ea, Fa), AG.mt(ea, Fb))), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), sp1, sp2)
213      Equal.trans(F.F64, SF.pick(F.F64, False{}, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), F.sm_case(x, y, sa, ea, ea, EQ{}), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), FR.pk_f(F.F64, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), Equal.trans(F.F64, F.sm_case(x, y, sa, ea, ea, EQ{}), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), imp, Equal.sym(F.F64, SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.sub_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea), Nat.cmp(Fa, Fb)), spc)))
214
215def core_c(+one: Nat, +h1: {one == 1n : Nat}, +x: F.F64, +y: F.F64, +sa: Bool, +sb: Bool, +ea: Nat, +eb: Nat, +Fa: Nat, +Fb: Nat, +hfa: {SW.value(F.frac(x)) == Fa : Nat}, +hfb: {SW.value(F.frac(y)) == Fb : Nat}, +hFa: {C.fits(52n, Fa) == True{} : Bool}, +hFb: {C.fits(52n, Fb) == True{} : Bool}, +hlta: {Nat.is_lt(ea, 2047n) == True{} : Bool}, +hltb: {Nat.is_lt(eb, 2047n) == True{} : Bool}, +sg: Bool, +hsg: {Bool.not(Bool.xor(sa, sb)) == sg : Bool}, +c: Cmp, +hc: {Nat.cmp(ea, eb) == c : Cmp}) -> {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, eb, c), F.sm_case(x, y, sa, ea, eb, c)) == SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))) : F.F64}:
216  match c:
217    case LT{}:
218      +hlt = NC.lt_of_cmp(ea, eb, hc)
219      +r = caseLT(one, h1, x, y, sa, sb, ea, eb, Fa, Fb, hfa, hfb, hFa, hFb, N.is_eq_lt(eb, 2047n, hltb), hlt, sg, hsg)
220      Equal.trans(F.F64, SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, eb, LT{}), F.sm_case(x, y, sa, ea, eb, LT{})), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), r, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), SF.add_mag(sa, AG.mt(ea, Fa), sb, C.shift(Nat.sub(AG.xe(eb), AG.xe(ea)), AG.mt(eb, Fb)), AG.xe(ea)), spec_lt(sa, sb, ea, eb, Fa, Fb, xe_le(ea, eb, hlt))))
221    case GT{}:
222      +hgt = NC.lt_of_gt(ea, eb, hc)
223      +r = caseGT(one, h1, x, y, sa, sb, ea, eb, Fa, Fb, hfa, hfb, hFa, hFb, N.is_eq_lt(ea, 2047n, hlta), hgt, sg, hsg)
224      Equal.trans(F.F64, SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, eb, GT{}), F.sm_case(x, y, sa, ea, eb, GT{})), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), r, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(eb), Nat.min(AG.xe(ea), AG.xe(eb))), AG.mt(eb, Fb)), Nat.min(AG.xe(ea), AG.xe(eb))), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), AG.xe(eb)), AG.mt(ea, Fa)), sb, AG.mt(eb, Fb), AG.xe(eb)), spec_gt(sa, sb, ea, eb, Fa, Fb, xe_le(eb, ea, hgt))))
225    case EQ{}:
226      +e = NC.eq_of_cmp(ea, eb, hc)
227      +r = caseEQ(one, h1, x, y, sa, sb, ea, Fa, Fb, hfa, hfb, hFa, hFb, hlta, sg, hsg)
228      +p = Equal.trans(F.F64, SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, ea, EQ{}), F.sm_case(x, y, sa, ea, ea, EQ{})), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fb)), Nat.min(AG.xe(ea), AG.xe(ea))), r, Equal.sym(F.F64, SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(ea))), AG.mt(ea, Fb)), Nat.min(AG.xe(ea), AG.xe(ea))), SF.add_mag(sa, AG.mt(ea, Fa), sb, AG.mt(ea, Fb), AG.xe(ea)), spec_eq(sa, sb, ea, Fa, Fb)))
229      L.subst(Nat, w => {SF.pick(F.F64, sg, F.am_case(x, y, sa, ea, w, EQ{}), F.sm_case(x, y, sa, ea, w, EQ{})) == SF.add_mag(sa, C.shift(Nat.sub(AG.xe(ea), Nat.min(AG.xe(ea), AG.xe(w))), AG.mt(ea, Fa)), sb, C.shift(Nat.sub(AG.xe(w), Nat.min(AG.xe(ea), AG.xe(w))), AG.mt(w, Fb)), Nat.min(AG.xe(ea), AG.xe(w))) : F.F64}, ea, eb, e, p)
230
231# F.add on finite operands is the spec's add_fin
232def afin(+xl: U32, +xh: U32, +yl: U32, +yh: U32, +ha: {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == True{} : Bool}, +hb: {Nat.is_lt(SF.efield(F.Bits{yl, yh}), 2047n) == True{} : Bool}) -> {F.add(F.Bits{xl, xh}, F.Bits{yl, yh}) == SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}) : F.F64}:
233  +e0 = ap(F.Bits{xl, xh}, F.Bits{yl, yh}, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))))
234  +c1 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(t, F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, t, F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), F.signbit(F.Bits{xl, xh}), SF.sign(F.Bits{xl, xh}), FB.signbit_value(F.Bits{xl, xh}))
235  +c2 = Equal.cong(Bool, F.F64, t => SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), t)), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), F.signbit(F.Bits{yl, yh}), SF.sign(F.Bits{yl, yh}), FB.signbit_value(F.Bits{yl, yh}))
236  +c3 = 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, F.exp_field(F.Bits{yl, yh}), Nat.cmp(t, F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), t, F.exp_field(F.Bits{yl, yh}), Nat.cmp(t, F.exp_field(F.Bits{yl, yh})))), F.exp_field(F.Bits{xl, xh}), SF.efield(F.Bits{xl, xh}), hea(xl, xh))
237  +c4 = 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))), F.exp_field(F.Bits{yl, yh}), SF.efield(F.Bits{yl, yh}), hea(yl, yh))
238  +r = core_c(1n, {==}, F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}), SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh}), SF.frac(F.Bits{xl, xh}), SF.frac(F.Bits{yl, yh}), hfr(xl, xh), hfr(yl, yh), hF(xl, xh), hF(yl, yh), ha, hb, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), SF.sign(F.Bits{yl, yh}))), {==}, Nat.cmp(SF.efield(F.Bits{xl, xh}), SF.efield(F.Bits{yl, yh})), {==})
239  Equal.trans(F.F64, F.add(F.Bits{xl, xh}, F.Bits{yl, yh}), SF.pick(F.F64, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), e0, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(F.signbit(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, F.signbit(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c1, Equal.trans(F.F64, SF.pick(F.F64, Bool.not(Bool.xor(SF.sign(F.Bits{xl, xh}), F.signbit(F.Bits{yl, yh}))), F.am_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(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}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c2, 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}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}))), F.sm_case(F.Bits{xl, xh}, F.Bits{yl, yh}, SF.sign(F.Bits{xl, xh}), F.exp_field(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(F.exp_field(F.Bits{xl, xh}), F.exp_field(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}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(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}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(F.Bits{yl, yh})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c3, 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}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(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}), F.exp_field(F.Bits{yl, yh}), Nat.cmp(SF.efield(F.Bits{xl, xh}), F.exp_field(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})))), SF.add_fin(F.Bits{xl, xh}, F.Bits{yl, yh}), c4, r)))))