law bit_lt32

lawful-words@0.1.0.0 · proof_bytes.bend:112

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

112# Bits from 32 up are clear.
113law bit_lt32:
114  for +a: U32
115  for +k: Nat
116  {D.bit(a, k) == Bool.and(Nat.is_lt(k, 32n), D.bit(a, k)) : Bool}