def bit_length_k

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u64int.bend:401

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/u64laws.bend as LW
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as WU
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/natfuel.bend as NF

401def bit_length_k(+k: Nat, +hk: {k == 64n : Nat}, +n: WU.U64) -> {G.bit_length(~WU.U64, ~I.u64_op, ~I.u64_is, n) == M.bit_length(v(n)) : Nat}:
402  +hj = L.subst(Nat, z => {Nat.is_le(z, 140n) == True{} : Bool}, 64n, k, Equal.sym(Nat, k, 64n, hk), {==})
403  Equal.trans(Nat, G.bit_length(~WU.U64, ~I.u64_op, ~I.u64_is, n), M.bit_length_go(140n, v(n), 0n), M.bit_length(v(n)), blsim(140n, 0n, n, I.u64_is(NM.IsZero{n}), v(n), {==}, {==}), NF.bl_140(k, v(n), hj, LW.val_lt(k, hk, n)))