def rne_top

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64round.bend:442

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/proofs/lib/nat.bend as N
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/w64sh.bend as SH

442# a 63-bit m rounds to at most 2^53
443def rne_top(+one: Nat, +h1: {one == 1n : Nat}, +m: Nat, +hm: {C.fits(63n, m) == True{} : Bool}) -> {Nat.is_le(SF.rne(m, 10n), C.shift(53n, one)) == True{} : Bool}:
444  +f = SH.fits_high(10n, 53n, m, hm)
445  N.le_trans(SF.rne(m, 10n), Nat.add(C.high(10n, m), 1n), C.shift(53n, one), rne_ub(m), succ_le(C.high(10n, m), C.shift(53n, one), WW.lt_one(53n, one, h1, C.high(10n, m), f)))