is_pow2_equiv

Function is_pow2_equiv 

Source
pub broadcast proof fn is_pow2_equiv(n: int)
Expand description
ensures
is_pow2(n) <==> is_pow2_exists(n),

Proof that the recursive and existential specifications for is_pow2 are equivalent.