F64addf.seq: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend as F64addf
Lines 173-194 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend&start_line=173&end_line=194

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/spec/math/w64.bend as SW
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend as WA
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend as NC
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adde.bend as AE
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend as AG

def 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}:
  match d:
    case EQ{}:
      AG.zero_v(False{})
    case GT{}:
      +hlt = NC.lt_of_gt(Fa, Fb, hd)
      +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)))
      +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)))
      +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)))
      +hz = AG.posz(Nat.sub(Fa, Fb), FR.lt_sub_pos(Fb, Fa, hlt))
      +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))
      +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))
      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)
    case LT{}:
      +hlt = NC.lt_of_cmp(Fa, Fb, hd)
      +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)))
      +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)))
      +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)))
      +hz = AG.posz(Nat.sub(Fb, Fa), FR.lt_sub_pos(Fa, Fb, hlt))
      +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))
      +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))
      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)

Uses (44):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.not
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.xor
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend&name=subst
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=le_lt_trans
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend&name=lt_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64adde.bend&name=smx
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend&name=hovm
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend&name=rc2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addf.bend&name=xem
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=mt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=posz
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=sgn
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=sub_le
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=xe
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64addg.bend&name=zero_v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lt_fit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=lt_sub_pos
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=sub_cancel_r
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=lt_of_cmp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/natcmp.bend&name=lt_of_gt
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64add.bend&name=sub_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=fits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=b2n
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=round
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sub_mag
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/w64.bend&name=value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=frac
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sm_eq2
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sm_exact
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/w64.bend&name=sub