import Base
import ./f64round.bend as FR
import ../../../spec/lib/common.bend as C
import ../../../spec/math/f64.bend as SF
import ../../../src/math/f64.bend as F
import ../../../src/math/w64.bend as X
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ./width.bend as WW
import ./natcmp.bend as NC
import ./f64bits.bend as FB
import ./f64addf.bend as AF

# Add.value and Sub.value of spec/math/f64.bend: SoftFloat's addF64 (the
# NaN, infinity and invalid cases of addMagsF64/subMagsF64) is the spec's
# add, IEEE 754-2019 §6.2/§7.2 on top of the finite case (f64addf.bend).

def v(+x: U32) -> Nat:
  U32.to_nat(x)

# the spec's add with the classification of both operands as Booleans
def 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:
  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)))

def pick_same(+b: Bool, +r: F.F64) -> {SF.pick(F.F64, b, r, r) == r : F.F64}:
  match b:
    case True{}:
      Equal.trans(F.F64, SF.pick(F.F64, True{}, r, r), r, r, FR.pk_t(F.F64, r, r), {==})
    case False{}:
      Equal.trans(F.F64, SF.pick(F.F64, False{}, r, r), r, r, FR.pk_f(F.F64, r, r), {==})

def 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}:
  {==}

def 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}:
  match z1:
    case True{}:
      {==}
    case False{}:
      {==}

def 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}:
  match z2:
    case True{}:
      {==}
    case False{}:
      {==}

def 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}:
  match z1 z2 sx sy:
    case True{} True{} True{} True{}:
      {==}
    case True{} True{} True{} False{}:
      {==}
    case True{} True{} False{} True{}:
      {==}
    case True{} True{} False{} False{}:
      {==}
    case True{} False{} True{} True{}:
      {==}
    case True{} False{} True{} False{}:
      {==}
    case True{} False{} False{} True{}:
      {==}
    case True{} False{} False{} False{}:
      {==}
    case False{} True{} True{} True{}:
      {==}
    case False{} True{} True{} False{}:
      {==}
    case False{} True{} False{} True{}:
      {==}
    case False{} True{} False{} False{}:
      {==}
    case False{} False{} True{} True{}:
      {==}
    case False{} False{} True{} False{}:
      {==}
    case False{} False{} False{} True{}:
      {==}
    case False{} False{} False{} False{}:
      {==}

# the spec's add, classified
def 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}:
  {==}

def 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}:
  FB.lt_ne(SF.efield(F.Bits{xl, xh}), 2047n, WW.low_lt(11n, C.high(20n, v(xh))))

def 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}:
  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))

# F.add as the SoftFloat case split on the spec's fields
def 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}:
  +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}))))
  +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}))
  +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}))
  +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))
  +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))
  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))))

def 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}:
  match a1 a2:
    case False{} False{}:
      +r = AF.afin(xl, xh, yl, yh, ltf(xl, xh, ha1), ltf(yl, yh, ha2))
      +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)
      +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)
      +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})))))
      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))
    case True{} False{}:
      +e1 = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, ha1)
      +hy = ltf(yl, yh, ha2)
      +i1 = add_g(xl, xh, yl, yh)
      +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)
      +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))
      +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})))))
      +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, {==}))
      +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)
      +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)
      +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))
      +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})))))))
      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))
    case False{} True{}:
      +e2 = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, ha2)
      +hx = ltf(xl, xh, ha1)
      +i1 = add_g(xl, xh, yl, yh)
      +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)
      +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))
      +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})))))
      +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, {==}))
      +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)
      +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)
      +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))
      +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})))))))
      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))
    case True{} True{}:
      +e1 = N.eq_from_is_eq(SF.efield(F.Bits{xl, xh}), 2047n, ha1)
      +e2 = N.eq_from_is_eq(SF.efield(F.Bits{yl, yh}), 2047n, ha2)
      +i1 = add_g(xl, xh, yl, yh)
      +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)
      +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)
      +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, {==}))
      +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, {==}))
      +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)
      +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)
      +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))
      +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})))))))
      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))

def add_value(+x: F.F64, +y: F.F64) -> SF.Add.value(x, y):
  match x y:
    case F.Bits{+xl, +xh} F.Bits{+yl, +yh}:
      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), {==})

def sub_value(+x: F.F64, +y: F.F64) -> SF.Sub.value(x, y):
  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)))