law inc_nat

stelliferous@0.0.2.0 · proofs/u32_successor.bend:24

import Base

24law inc_nat:
25  for +n: Nat
26  for +w: Word(n)
27  {Word.to_nat(1n+n,Word.inc(1n+n,Word.shr.pad(n,w))) == 1n+Word.to_nat(n,w) : Nat}