law byte_shln_low

lawful-words@0.1.0.0 · LAWS.bend:430

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

430law byte_shln_low:
431  for w: U32
432  for s: Nat
433  for j: Nat
434  for hj: {Nat.is_lt(j, s) == True{} : Bool}
435  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == 0 : U32}