Function vstd::std_specs::bits::axiom_u16_trailing_zeros

pub broadcast proof fn axiom_u16_trailing_zeros(i: u16)

Expand description

ensures

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

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

0 <= u16_trailing_zeros(i) < 16 ==> (i >> u16_trailing_zeros(i) as u16) & 1u16 == 1u16,

i << sub(16, u16_trailing_zeros(i) as u16) == 0,

forall |j: u16| 0 <= j < u16_trailing_zeros(i) ==> #[trigger] (i >> j) & 1u16 == 0u16,