law word_value_eq

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

import Base

77law word_value_eq:
78  for +n: Nat
79  for +a: Word(n)
80  for +b: Word(n)
81  for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
82  {a == b : Word(n)}