lemma_u32_pow2_ilog2_x

vstd_extra::external::ilog2

Function lemma_u32_pow2_ilog2_x 

Source 
pub broadcast proof fn lemma_u32_pow2_ilog2_x(e: u32, x: u32)
Expand description
requires
#[trigger] pow2(e as nat) == x,
ensures
#[trigger] x.ilog2() == e,