def shr_pow2u

bend-collections-laws-math@1.0.0.0 · proofs/lib/u32.bend:175

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
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

175def shr_pow2u(+p: Nat, +h: {Nat.is_lt(1n+p, 32n) == True{} : Bool}) -> {U32.shr(pow2u(1n+p)) == pow2u(p) : U32}:
176  injective(U32.shr(pow2u(1n+p)), pow2u(p),
177    Equal.trans(Nat, U32.to_nat(U32.shr(pow2u(1n+p))), SC.pow2(p), U32.to_nat(pow2u(p)),
178      N.bit_split_val(low_bit(pow2u(1n+p)), False{}, U32.to_nat(U32.shr(pow2u(1n+p))), SC.pow2(p),
179        Equal.trans(Nat, Nat.add(S.bit_value(low_bit(pow2u(1n+p))), Nat.double(U32.to_nat(U32.shr(pow2u(1n+p))))), U32.to_nat(pow2u(1n+p)), Nat.double(SC.pow2(p)),
180          Equal.sym(Nat, U32.to_nat(pow2u(1n+p)), Nat.add(S.bit_value(low_bit(pow2u(1n+p))), Nat.double(U32.to_nat(U32.shr(pow2u(1n+p))))), shr_split(pow2u(1n+p))),
181          pow2u_value(1n+p, h))),
182      Equal.sym(Nat, U32.to_nat(pow2u(p)), SC.pow2(p), pow2u_value(p, N.lt_trans(p, 1n+p, 32n, N.lt_succ(p), h)))))