law bit_not

lawful-words@0.1.0.0 · proof_u32.bend:1308

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

1308law bit_not:
1309  for +a: U32
1310  for +k: Nat
1311  {D.bit(U32.not(a), k) == (Nat.is_lt(k, 32n) && Bool.not(D.bit(a, k))) : Bool}