def ldf_c

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

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

227def ldf_c(+x: F.F64, +neg: Bool, +k: Nat) -> {F.ld_fin(x, neg, k) == LD(x, neg, k) : F.F64}:
228  match neg:
229    case True{}:
230      ldn_c(x, k, Nat.is_lt(F.dexp(x), Nat.add(k, 63n)), {==})
231    case False{}:
232      +hu = N.le_trans(63n, F.dexp(x), Nat.add(F.dexp(x), k), T.dexp_ge(x), N.le_add_right(F.dexp(x), k))
233      +e1 = rwx(x, Nat.add(F.dexp(x), k), hu)
234      +e2 = Equal.cong(Nat, F.F64, t => SF.round(SF.sign(x), SF.mant(x), Nat.add(t, k)), F.dexp(x), SF.xexp(x), T.dexp_value(x))
235      Equal.trans(F.F64, F.round_w(F.signbit(x), Nat.add(F.dexp(x), k), F.dmant(x)), SF.round(SF.sign(x), SF.mant(x), Nat.add(F.dexp(x), k)), LD(x, False{}, k), e1, e2)