def dec

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64fmod.bend:198

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

198def dec(+x: F.F64) -> {x == SF.encode(SF.sign(x), SF.efield(x), SF.frac(x)) : F.F64}:
199  match x:
200    case F.Bits{+l, +h}:
201      +H = v(h)
202      +H20 = C.high(20n, H)
203      +e1 = WW.low_high(20n, H)
204      +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))
205      +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)))
206      +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)
207      +a1 = Nat.add(C.low(20n, H), C.shift(20n, H20))
208      +a2 = Nat.add(C.low(20n, H), C.shift(20n, Nat.add(C.low(11n, H20), C.shift(11n, C.high(11n, H20)))))
209      +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}))))))
210      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)))