law word_not_add_sym

bend-mathlib@0.8.1.0 · u32.bend:995

import Base

995# One plus a word plus its complement is two to the width: 1 + to_nat (not w) + to_nat w = 2^n, reversed to rewrite toward the simple side.
996law word_not_add_sym:
997  for n: Nat
998  for w: Word(n)
999  {Nat.pow(2n, n) == 1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) : Nat}