law to_nat_and_mask

lawful-words@0.1.0.0 · proof_u32.bend:1159

import Base

1159law to_nat_and_mask:
1160  for +a: U32
1161  for +m: U32
1162  for +k: Nat
1163  for +h: {U32.to_nat(m) == Nat.sub(Nat.pow(2n, k), 1n) : Nat}
1164  {U32.to_nat(U32.and(a, m)) == Nat.mod(U32.to_nat(a), Nat.pow(2n, k)) : Nat}