law to_nat_byte

lawful-words@0.1.0.0 · proof_bytes.bend:545

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

545law to_nat_byte:
546  for +w: U32
547  for +j: Nat
548  {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}