law word_not_value

bend-osdev-u32@0.1.0.0 · LAWS.bend:90

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

90law word_not_value:
91  for +n: Nat
92  for +w: Word(n)
93  {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == U.U32Nat.dbl(n, 1n) : Nat}