law wsub_val

lawful-words@0.1.0.0 · proof_word.bend:515

import Base

515# (a + 2^n) - b = 1 + a + not b.
516law wsub_val:
517  for +n: Nat
518  for +a: Word(n)
519  for +b: Word(n)
520  {Nat.sub(Nat.add(Word.to_nat(n, a), Nat.pow(2n, n)), Word.to_nat(n, b))
521    == 1n+Nat.add(Word.to_nat(n, a), Word.to_nat(n, Word.not(n, b))) : Nat}