law bit_shl1

lawful-words@0.1.0.0 · proof_bytes.bend:182

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

182law bit_shl1:
183  for +a: U32
184  for +j: Nat
185  {D.bit(U32.shl(a), 1n+j) == Bool.and(Nat.is_lt(1n+j, 32n), D.bit(a, j)) : Bool}