~/jendhub

def hlf_bound

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32half.bend:109

import bend-collections-laws-math@1.0.0.0/proofs/lib/u32half.bend as U32half
import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC

109def hlf_bound(+i: Nat, +k: Nat, +h: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}) -> {Nat.is_lt(hlf(i), SC.pow2(k)) == True{} : Bool}:
110  N.le_lt_trans(hlf(i), i, SC.pow2(k), hlf_le(i), h)

Uses (7)

Used by (1)