law to_nat_shln

import lawful-words@0.1.0.0/LAWS.bend as LAWS

import Base

204law to_nat_shln:
205  for a: U32
206  for k: Nat
207  {U32.to_nat(U32.shln(a, k)) == Nat.mod(Nat.mul(U32.to_nat(a), Nat.pow(2n, k)), Nat.pow(2n, 32n)) : Nat}

Uses (8)

U32
Nat
U32.to_nat
Nat.mul
Nat.mod
…

Used by (0)

No other definition uses this definition.