Function vstd::bits::lemma_low_bits_mask_unfold

source · 
pub broadcast proof fn lemma_low_bits_mask_unfold(n: nat)
Expand description
requires
n > 0,
ensures
#[trigger] low_bits_mask(n) == 2 * low_bits_mask((n - 1) as nat) + 1,

Proof relating the n-bit mask to a function of the (n-1)-bit mask.