F64addf.ap: 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 44-49 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=44&end_line=49

import Base
import bend-collections-laws-math@1.0.0.0/spec/math/f64.bend as SF
import bend-collections-laws-math@1.0.0.0/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend as FR

def ap(+x: F.F64, +y: F.F64, +same: Bool) -> {F.add_pick(x, y, same) == SF.pick(F.F64, same, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))) : F.F64}:
  match same:
    case True{}:
      Equal.trans(F.F64, F.add_pick(x, y, True{}), F.add_mags(x, y, F.signbit(x)), SF.pick(F.F64, True{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), {==}, Equal.sym(F.F64, SF.pick(F.F64, True{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), F.add_mags(x, y, F.signbit(x)), FR.pk_t(F.F64, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x)))))
    case False{}:
      Equal.trans(F.F64, F.add_pick(x, y, False{}), F.sub_mags(x, y, F.signbit(x)), SF.pick(F.F64, False{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), {==}, Equal.sym(F.F64, SF.pick(F.F64, False{}, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x))), F.sub_mags(x, y, F.signbit(x)), FR.pk_f(F.F64, F.add_mags(x, y, F.signbit(x)), F.sub_mags(x, y, F.signbit(x)))))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=pk_f
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64round.bend&name=pk_t
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=pick
  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=add_mags
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=add_pick
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=signbit
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=sub_mags