law word_not_add

bend-mathlib@0.8.1.0 · u32.bend:147

import Base

147# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n.
148law word_not_add:
149  for n: Nat
150  for w: Word(n)
151  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == Nat.pow(2n, n) : Nat}