law word_inc_exact_sym

bend-mathlib@0.8.1.0 · u32.bend:1060

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

1060# Increment is exact without overflow: 1 + w < 2^n implies to_nat (inc w) = 1 + w, reversed to rewrite toward the simple side.
1061law word_inc_exact_sym:
1062  for n: Nat
1063  for w: Word(n)
1064  for h: MNat.lt(1n+Word.to_nat(n, w), Nat.pow(2n, n))
1065  {1n+Word.to_nat(n, w) == Word.to_nat(n, Word.inc(n, w)) : Nat}