def bit_length_k

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32int.bend:400

import Base
import bend-collections-laws-math@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-math@1.0.0.0/src/math/num.bend as NM
import bend-collections-laws-math@1.0.0.0/src/math/natural.bend as M
import bend-collections-laws-math@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/u32.bend as U32P
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

400def bit_length_k(+k: Nat, +hk: {k == 32n : Nat}, +n: U32) -> {G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n) == M.bit_length(v(n)) : Nat}:
401  +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 32n, k, Equal.sym(Nat, k, 32n, hk), {==})
402  Equal.trans(Nat, G.bit_length(~U32, ~I.u32_op, ~I.u32_is, n), M.bit_length_go(140n, v(n), 0n), M.bit_length(v(n)), blsim(140n, 0n, n, I.u32_is(NM.IsZero{n}), v(n), {==}, {==}), NF.bl_140(k, v(n), hj, U32P.val_lt(1n, {==}, k, hk, n)))