law byte_shrn

lawful-words@0.1.0.0 · proof_bytes.bend:682

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

682law byte_shrn:
683  for +w: U32
684  for +s: Nat
685  for +j: Nat
686  {D.byte(U32.shrn(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.add(j, s)) : U32}