law adc_zero

stelliferous@0.0.2.0 · proofs/u32_successor.bend:42

import Base

42law adc_zero:
43  for +n: Nat
44  for +w: Word(n)
45  {Word.adc(n,w,Word.zero(n),False{},False{}) == w : Word(n)}