law byte_shln_high

lawful-words@0.1.0.0 · proof_bytes.bend:734

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

734law byte_shln_high:
735  for +w: U32
736  for +s: Nat
737  for +j: Nat
738  for +hs: {Nat.is_le(s, j) == True{} : Bool}
739  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
740  {D.byte(U32.shln(w, Nat.mul(8n, s)), j) == D.byte(w, Nat.sub(j, s)) : U32}