law word_inc_nat

bend-kit-lemmas@0.1.1.0 · lemmas.bend:656

import Base
import bend-mathlib@0.7.4.0/nat.bend as MNat

656# Incrementing without overflow adds one.
657law word_inc_nat:
658  for n: Nat
659  for w: Word(n)
660  for h: MNat.lt(1n+Word.to_nat(n, w), pow2(n))
661  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}