law u32_add_word

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

import Base

484law u32_add_word:
485  for -x: Word(32n)
486  for -y: Word(32n)
487  {Word.to_nat(32n, Word.add(32n, x, y)) == U32.to_nat(U32.add(U32{x}, U32{y})) : Nat}