Function vstd::std_specs::bits::axiom_u16_leading_zeros

pub broadcast proof fn axiom_u16_leading_zeros(i: u16)

Expand description

ensures

0 <= #[trigger] u16_leading_zeros(i) <= 16,

i == 0 <==> u16_leading_zeros(i) == 16,

0 <= u16_leading_zeros(i) < 16
    ==> (i >> sub(15u16, u16_leading_zeros(i) as u16)) & 1u16 != 0u16,

i >> sub(16, u16_leading_zeros(i) as u16) == 0,

forall |j: u16| {
    16 - u16_leading_zeros(i) <= j < 16 ==> #[trigger] (i >> j) & 1u16 == 0u16
},