law byte_shln_low

lawful-words@0.1.0.0 · proof_bytes.bend:706

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

706law byte_shln_low:
707  for +w: U32
708  for +s: Nat
709  for +j: Nat
710  for +hj: {Nat.is_lt(j, s) == True{} : Bool}
711  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == 0 : U32}