~/jendhub

proofs/math/typed/f64addv.bend

bend-collections-laws-math@1.0.0.0 · 157 lines · 14 definitions

1import Base
2import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
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/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/proofs/lib/nat.bend as N
8import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
10import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
11import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB
12import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as AF
13
14# Add.value and Sub.value of spec/math/f64.bend: SoftFloat's addF64 (the
15# NaN, infinity and invalid cases of addMagsF64/subMagsF64) is the spec's
16# add, IEEE 754-2019 §6.2/§7.2 on top of the finite case (f64addf.bend).
17
18def v(+x: U32) -> Nat:
19  U32.to_nat(x)
20
21# the spec's add with the classification of both operands as Booleans
22def spec_g(+a1: Bool, +z1: Bool, +a2: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> F.F64:
23  SF.pick(F.F64, Bool.or(Bool.and(a1, Bool.not(z1)), Bool.and(a2, Bool.not(z2))), SF.qnan(), SF.pick(F.F64, Bool.and(a1, z1), SF.pick(F.F64, Bool.and(Bool.and(a2, z2), Bool.not(Bool.not(Bool.xor(sx, sy)))), SF.qnan(), x), SF.pick(F.F64, Bool.and(a2, z2), y, fin)))
24
25def pick_same(+b: Bool, +r: F.F64) -> {SF.pick(F.F64, b, r, r) == r : F.F64}:
26  match b:
27    case True{}:
28      Equal.trans(F.F64, SF.pick(F.F64, True{}, r, r), r, r, FR.pk_t(F.F64, r, r), {==})
29    case False{}:
30      Equal.trans(F.F64, SF.pick(F.F64, False{}, r, r), r, r, FR.pk_f(F.F64, r, r), {==})
31
32def ff(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {spec_g(False{}, z1, False{}, z2, sx, sy, x, y, fin) == fin : F.F64}:
33  {==}
34
35def tf(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {F.nan_or(x, Bool.not(z1)) == spec_g(True{}, z1, False{}, z2, sx, sy, x, y, fin) : F.F64}:
36  match z1:
37    case True{}:
38      {==}
39    case False{}:
40      {==}
41
42def ft(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {F.nan_or(y, Bool.not(z2)) == spec_g(False{}, z1, True{}, z2, sx, sy, x, y, fin) : F.F64}:
43  match z2:
44    case True{}:
45      {==}
46    case False{}:
47      {==}
48
49def tt(+z1: Bool, +z2: Bool, +sx: Bool, +sy: Bool, +x: F.F64, +y: F.F64, +fin: F.F64) -> {SF.pick(F.F64, Bool.not(Bool.xor(sx, sy)), F.nan_or(x, Bool.or(Bool.not(z1), Bool.not(z2))), F.nan()) == spec_g(True{}, z1, True{}, z2, sx, sy, x, y, fin) : F.F64}:
50  match z1 z2 sx sy:
51    case True{} True{} True{} True{}:
52      {==}
53    case True{} True{} True{} False{}:
54      {==}
55    case True{} True{} False{} True{}:
56      {==}
57    case True{} True{} False{} False{}:
58      {==}
59    case True{} False{} True{} True{}:
60      {==}
61    case True{} False{} True{} False{}:
62      {==}
63    case True{} False{} False{} True{}:
64      {==}
65    case True{} False{} False{} False{}:
66      {==}
67    case False{} True{} True{} True{}:
68      {==}
69    case False{} True{} True{} False{}:
70      {==}
71    case False{} True{} False{} True{}:
72      {==}
73    case False{} True{} False{} False{}:
74      {==}
75    case False{} False{} True{} True{}:
76      {==}
77    case False{} False{} True{} False{}:
78      {==}
79    case False{} False{} False{} True{}:
80      {==}
81    case False{} False{} False{} False{}:
82      {==}
83
84# the spec's add, classified
85def spec_c(+xl: U32, +xh: U32, +yl: U32, +yh: U32) -> {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})) : F.F64}:
86  {==}
87
88def lt11(+xl: U32, +xh: U32) -> {Nat.is_lt(SF.efield(F.Bits{xl, xh}), 2047n) == Bool.not(Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n)) : Bool}:
89  FB.lt_ne(SF.efield(F.Bits{xl, xh}), 2047n, WW.low_lt(11n, C.high(20n, v(xh))))
90
91def 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}:
92  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{}, lt11(xl, xh), Equal.cong(Bool, Bool, t => Bool.not(t), Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), False{}, h))
93
94# F.add as the SoftFloat case split on the spec's fields
95def add_g(+xl: U32, +xh: U32, +yl: U32, +yh: U32) -> {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})))) : F.F64}:
96  +e0 = AF.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}))))
97  +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}))
98  +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}))
99  +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}), AF.hea(xl, xh))
100  +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}), AF.hea(yl, yh))
101  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.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})))), 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.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})))), 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.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})))), 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.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})))), c3, c4))))
102
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))
150
151def add_value(+x: F.F64, +y: F.F64) -> SF.Add.value(x, y):
152  match x y:
153    case F.Bits{+xl, +xh} F.Bits{+yl, +yh}:
154      top_c(xl, xh, yl, yh, Nat.is_eq(SF.efield(F.Bits{xl, xh}), 2047n), {==}, Nat.is_eq(SF.efield(F.Bits{yl, yh}), 2047n), {==})
155
156def sub_value(+x: F.F64, +y: F.F64) -> SF.Sub.value(x, y):
157  Equal.trans(F.F64, F.add(x, F.neg(y)), F.add(x, SF.neg(y)), SF.add(x, SF.neg(y)), Equal.cong(F.F64, F.F64, z => F.add(x, z), F.neg(y), SF.neg(y), FB.neg_value(y)), add_value(x, SF.neg(y)))