law bit_shln

lawful-words@0.1.0.0 · proof_bytes.bend:198

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

198law bit_shln:
199  for +a: U32
200  for +s: Nat
201  for +k: Nat
202  {D.bit(U32.shln(a, s), k) == Bool.and(Nat.is_le(s, k), Bool.and(Nat.is_lt(k, 32n), D.bit(a, Nat.sub(k, s)))) : Bool}