law bit_shrn

lawful-words@0.1.0.0 · proof_bytes.bend:128

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

128law bit_shrn:
129  for +a: U32
130  for +s: Nat
131  for +k: Nat
132  {D.bit(U32.shrn(a, s), k) == D.bit(a, Nat.add(k, s)) : Bool}