law word_shr_value

bend-osdev-u32@0.1.0.0 · LAWS.bend:136

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

136law word_shr_value:
137  for +n: Nat
138  for +w: Word(n)
139  {Word.to_nat(n, Word.shr(n, w)) == U.U32Nat.half(Word.to_nat(n, w)) : Nat}