def frac_v

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64modf.bend:56

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

56def frac_v(+x: F.F64) -> {F.mf_frac(F.signbit(x), F.dmant(x), F.dexp(x), Nat.sub(3000n, F.dexp(x)), Nat.is_lt(Nat.sub(3000n, F.dexp(x)), 64n)) == FRAC(x) : F.F64}:
57  +k = Nat.sub(3000n, F.dexp(x))
58  +e0 = mfr_c(F.signbit(x), F.dmant(x), F.dexp(x), T.dexp_ge(x), k, Nat.is_lt(k, 64n), {==})
59  +e1 = Equal.cong(Bool, F.F64, t => SF.round(t, C.low(k, SW.value(F.dmant(x))), F.dexp(x)), F.signbit(x), SF.sign(x), FB.signbit_value(x))
60  +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), C.low(k, t), F.dexp(x)), SW.value(F.dmant(x)), SF.mant(x), T.dmant_value(x))
61  +e3 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), C.low(Nat.sub(3000n, t), SF.mant(x)), t), F.dexp(x), SF.xexp(x), T.dexp_value(x))
62  +r0 = SF.round(F.signbit(x), C.low(k, SW.value(F.dmant(x))), F.dexp(x))
63  +r1 = SF.round(SF.sign(x), C.low(k, SW.value(F.dmant(x))), F.dexp(x))
64  +r2 = SF.round(SF.sign(x), C.low(k, SF.mant(x)), F.dexp(x))
65  Equal.trans(F.F64, F.mf_frac(F.signbit(x), F.dmant(x), F.dexp(x), k, Nat.is_lt(k, 64n)), r0, FRAC(x), e0, Equal.trans(F.F64, r0, r1, FRAC(x), e1, Equal.trans(F.F64, r1, r2, FRAC(x), e2, e3)))