law encode_add

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:60

import Base

60law encode_add:
61  for +a: Nat
62  for +b: Nat
63  for +width: Nat
64  {Word.add(width,encode(a,width),encode(b,width)) == encode(Nat.add(a,b),width) : Word(width)}