def bl_le_n

bend-collections-laws-crypto@1.0.0.0 · proofs/math/typed/natfuel.bend:559

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/bits.bend as BT

559def bl_le_n(+K: Nat, +n: Nat, +hn: {Nat.is_lt(n, C.pow2(K)) == True{} : Bool}) -> {Nat.is_le(M.bit_length(n), K) == True{} : Bool}:
560  match n:
561    case 0n:
562      L.subst(Nat, z => {Nat.is_le(z, K) == True{} : Bool}, 0n, M.bit_length(0n), Equal.sym(Nat, M.bit_length(0n), 0n, BT.bit_length_zero()), N.zero_le(K))
563    case 1n+ +np:
564      +bl = M.bit_length(1n+np)
565      +h = N.le_lt_trans(C.pow2(bl), Nat.double(1n+np), C.pow2(1n+K), BT.bit_length_le(np), N.double_lt(1n+np, C.pow2(K), hn))
566      bl_le_c(K, bl, h, Nat.is_le(1n+K, bl), {==})