Function vstd::std_specs::bits::axiom_u16_trailing_zeros
source · 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,