def rwx

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64exp.bend:193

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/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/proofs/math/typed/f64bits.bend as FB
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/f64tools.bend as T

193# the round_w of the significand at scale u is the spec's round at u
194def rwx(+x: F.F64, +u: Nat, +hu: {Nat.is_le(63n, u) == True{} : Bool}) -> {F.round_w(F.signbit(x), u, F.dmant(x)) == SF.round(SF.sign(x), SF.mant(x), u) : F.F64}:
195  +a1 = T.rw_value(F.signbit(x), u, F.dmant(x), hu)
196  +a2 = Equal.cong(Bool, F.F64, t => SF.round(t, SW.value(F.dmant(x)), u), F.signbit(x), SF.sign(x), FB.signbit_value(x))
197  +a3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), t, u), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
198  Equal.trans(F.F64, F.round_w(F.signbit(x), u, F.dmant(x)), SF.round(F.signbit(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SF.mant(x), u), a1, Equal.trans(F.F64, SF.round(F.signbit(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SW.value(F.dmant(x)), u), SF.round(SF.sign(x), SF.mant(x), u), a2, a3))