law word_cmp_value

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

import Base

84law word_cmp_value:
85  for +n: Nat
86  for +a: Word(n)
87  for +b: Word(n)
88  {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}