law word_inc_exact

bend-mathlib@0.8.1.0 · u32.bend:401

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

401# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w.
402law word_inc_exact:
403  for n: Nat
404  for w: Word(n)
405  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
406  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}