law adc_one

stelliferous@0.0.2.0 · proofs/u32_successor.bend:60

import Base

60law adc_one:
61  for +n: Nat
62  for +w: Word(n)
63  {Word.adc(n,w,Word.zero(n),False{},True{}) == Word.inc(n,w) : Word(n)}