law add_one

stelliferous@0.0.2.0 · proofs/u32_successor.bend:78

import Base

78law add_one:
79  for +n: Nat
80  for +w: Word(n)
81  {Word.add(n,w,Word.inc(n,Word.zero(n))) == Word.inc(n,w) : Word(n)}