law word_inc_value

bend-osdev-u32@0.1.0.0 · LAWS.bend:122

import Base

122law word_inc_value:
123  for +n: Nat
124  for +w: Word(n)
125  for +z: Word(n)
126  for h: {Nat.is_le(1n+Word.to_nat(n, w), Word.to_nat(n, z)) == True{} : Bool}
127  {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}