law word_value_lt

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

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

72law word_value_lt:
73  for +n: Nat
74  for +w: Word(n)
75  {Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(n, 1n)) == True{} : Bool}