law wnot

lawful-words@0.1.0.0 · proof_word.bend:482

import Base

482# not w and w add up to 2^n - 1.
483law wnot:
484  for +n: Nat
485  for +w: Word(n)
486  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}