~/jendhub

def hj_of

bend-collections-laws-math@1.0.0.0 · proofs/math/random/float.bend:267

import bend-collections-laws-math@1.0.0.0/proofs/math/random/float.bend as Float
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/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L

267# j <= 52 from the bit length 1 + j <= 53
268def hj_of(+np: Nat, +j: Nat, +hf: {C.fits(53n, 1n+np) == True{} : Bool}, +hbl: {M.bit_length(1n+np) == 1n+j : Nat}) -> {Nat.is_le(j, 52n) == True{} : Bool}:
269  L.subst(Nat, z => {Nat.is_le(z, 53n) == True{} : Bool}, M.bit_length(1n+np), 1n+j, hbl, bl_le(53n, 1n+np, hf))

Uses (7)

Used by (1)