law wbit_not

lawful-words@0.1.0.0 · proof_word.bend:895

import Base

895law wbit_not:
896  for +n: Nat
897  for +a: Word(n)
898  for +k: Nat
899  {wbit(n, Word.not(n, a), k) == Bool.and(Nat.is_lt(k, n), Bool.not(wbit(n, a, k))) : Bool}