law w_and_mask

lawful-arrays@0.1.0.0 · proof_words.bend:43

import Base

43law w_and_mask:
44  for +a: U32
45  for +m: U32
46  for +k: Nat
47  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
48  {U32.to_nat(U32.and(a, m)) == Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) : Nat}