law bit_not

lawful-words@0.1.0.0 · LAWS.bend:306

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

306# not flips the 32 bits, and only those.
307law bit_not:
308  for a: U32
309  for k: Nat
310  {D.bit(U32.not(a), k) == (Nat.is_lt(k, 32n) && Bool.not(D.bit(a, k))) : Bool}