law to_nat_byte

lawful-words@0.1.0.0 · LAWS.bend:323

import Base
import lawful-words@0.1.0.0/defs.bend as D

323law to_nat_byte:
324  for w: U32
325  for j: Nat
326  {U32.to_nat(D.byte(w, j)) == Nat.mod(Nat.div(U32.to_nat(w), Nat.pow(2n, Nat.mul(8n, j))), Nat.pow(2n, 8n)) : Nat}