law word_inc_wrap

bend-mathlib@0.8.1.0 · u32.bend:413

import Base

413# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n.
414law word_inc_wrap:
415  for n: Nat
416  for w: Word(n)
417  {Word.to_nat(n, Word.inc(n, w)) == Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) : Nat}