def bl_fin_v
bend-collections-laws-math@1.0.0.0 · proofs/math/typed/w64clz.bend:140
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64clz.bend as W64clz
import Base
import bend-collections-laws-math@1.0.0.0/src/math/w64.bend as X
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
import bend-collections-laws-math@1.0.0.0/proofs/math/typed/w64sqrt.bend as W64S
140def bl_fin_v(+x: U32, p: INV(1n, v(x), S5(x))) -> {X.bl_fin(S5(x)) == M.bit_length(v(x)) : Nat}:
141 (a, b) = p
142 +em0 = small_c(P2(S5(x)), U32.is_lt(P2(S5(x)), 1), {==}, v(P2(S5(x))), {==}, b)
143 +em = L.subst(U32, w => {v(w) == M.bit_length(v(P2(S5(x)))) : Nat}, Bool.pick(U32, U32.is_lt(P2(S5(x)), 1), P2(S5(x)), 1), U32.min(P2(S5(x)), 1), Equal.sym(U32, U32.min(P2(S5(x)), 1), Bool.pick(U32, U32.is_lt(P2(S5(x)), 1), P2(S5(x)), 1), W64S.min_pick(P2(S5(x)), 1)), em0)
144 Equal.trans(Nat, X.bl_fin(S5(x)), X.bl_fin((P1(S5(x)), P2(S5(x)))), M.bit_length(v(x)), eta_fin(S5(x)), Equal.trans(Nat, Nat.add(P1(S5(x)), v(U32.min(P2(S5(x)), 1))), Nat.add(P1(S5(x)), M.bit_length(v(P2(S5(x))))), M.bit_length(v(x)), Equal.cong(Nat, Nat, z => Nat.add(P1(S5(x)), z), v(U32.min(P2(S5(x)), 1)), M.bit_length(v(P2(S5(x)))), em), Equal.sym(Nat, M.bit_length(v(x)), Nat.add(P1(S5(x)), M.bit_length(v(P2(S5(x))))), a)))