lemma_u64_is_pow2_is_ilog2_pow2

vstd_extra::external::ilog2

Function lemma_u64_is_pow2_is_ilog2_pow2 

Source 
pub broadcast proof fn lemma_u64_is_pow2_is_ilog2_pow2(x: u64)
Expand description
requires
#[trigger] is_pow2(x as int),
ensures
x as nat == pow2(x.ilog2() as nat),