F64fmod.dec: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend as F64fmod
Lines 198-210 of bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend&start_line=198&end_line=210

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/src/math/f64.bend as F
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend as WW
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend as FB

def dec(+x: F.F64) -> {x == SF.encode(SF.sign(x), SF.efield(x), SF.frac(x)) : F.F64}:
  match x:
    case F.Bits{+l, +h}:
      +H = v(h)
      +H20 = C.high(20n, H)
      +e1 = WW.low_high(20n, H)
      +e2 = Equal.cong(Nat, Nat, t => Nat.add(C.low(20n, H), C.shift(20n, t)), H20, Nat.add(C.low(11n, H20), C.shift(11n, C.high(11n, H20))), WW.low_high(11n, H20))
      +e3 = Equal.trans(Nat, C.high(11n, H20), C.high(31n, H), SF.b2n(SF.sign(F.Bits{l, h})), Equal.sym(Nat, C.high(Nat.add(20n, 11n), H), C.high(11n, H20), WW.high_comp(11n, 20n, H)), FB.bit_c(C.high(31n, H), FB.half0(h)))
      +e4 = Equal.cong(Nat, Nat, t => Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, t)))), C.high(11n, H20), SF.b2n(SF.sign(F.Bits{l, h})), e3)
      +a1 = Nat.add(C.low(20n, H), C.shift(20n, H20))
      +a2 = Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, C.high(11n, H20)))))
      +a3 = Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, SF.b2n(SF.sign(F.Bits{l, h}))))))
      FB.enc_g(l, h, SF.sign(F.Bits{l, h}), h, Equal.trans(Nat, H, a1, a3, e1, Equal.trans(Nat, a1, a2, a3, e2, e4)))

Uses (20):
  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=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=bit_c
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=enc_g
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64bits.bend&name=half0
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64fmod.bend&name=v
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=high_comp
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/typed/width.bend&name=low_high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=high
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/lib/common.bend&name=low
  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=efield
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=frac
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/spec/math/f64.bend&name=sign
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/f64.bend&name=F64