law byte_shln_high

lawful-words@0.1.0.0 · LAWS.bend:422

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

422law byte_shln_high:
423  for w: U32
424  for s: Nat
425  for j: Nat
426  for hs: {Nat.is_le(s, j) == True{} : Bool}
427  for hj: {Nat.is_lt(j, 4n) == True{} : Bool}
428  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.sub(j, s)) : U32}