law wadd_mod

lawful-words@0.1.0.0 · proof_word.bend:682

import Base

682law wadd_mod:
683  for +n: Nat
684  for +a: Word(n)
685  for +b: Word(n)
686  {Word.to_nat(n, Word.add(n, a, b)) == Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Nat.pow(2n, n)) : Nat}