law word_inc_wrap_sym

bend-mathlib@0.8.1.0 · u32.bend:1070

import Base

1070# Increment wraps modulo 2^n: to_nat (inc w) = (1 + w) % 2^n, reversed to rewrite toward the simple side.
1071law word_inc_wrap_sym:
1072  for n: Nat
1073  for w: Word(n)
1074  {Nat.mod(1n+Word.to_nat(n, w), Nat.pow(2n, n)) == Word.to_nat(n, Word.inc(n, w)) : Nat}