law to_nat_shln_mod

lawful-words@0.1.0.0 · LAWS.bend:215

import Base

215# A left shift by k leaves the low k bits zero.
216law to_nat_shln_mod:
217  for a: U32
218  for k: Nat
219  {Nat.mod(U32.to_nat(U32.shln(a, k)), Nat.pow(2n, k)) == 0n : Nat}