law word_add_mod

bend-kit-lemmas@0.1.1.0 · lemmas.bend:471

import Base

471# Addition wraps modulo 2^n.
472law word_add_mod:
473  for +n: Nat
474  for +a: Word(n)
475  for +b: Word(n)
476  {Word.to_nat(n, Word.add(n, a, b)) ==
477    Nat.mod(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), pow2(n)) : Nat}