Skip to main content

lemma_u16_and_zero

vstd_extra::bits

Function lemma_u16_and_zero 

Source 
pub proof fn lemma_u16_and_zero(x: u16)
Expand description
ensures
0u16 & x == 0u16,

AND-ing the zero word with any word is zero.