law word_not_nat

bend-kit-lemmas@0.1.1.0 · lemmas.bend:520

import Base

520# The bitwise complement of w has value 2^n - 1 - w.
521law word_not_nat:
522  for n: Nat
523  for w: Word(n)
524  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == pow2(n) : Nat}