law word_to_nat_lt

bend-mathlib@0.8.1.0 · u32.bend:17

import bend-mathlib@0.8.1.0/u32.bend as U32

import Base
import bend-mathlib@0.8.1.0/nat.bend as MNat

17# A word's value is below two to the width: to_nat w < 2^n.
18law word_to_nat_lt:
19  for n: Nat
20  for w: Word(n)
21  MNat.lt(Word.to_nat(n, w), Nat.pow(2n, n))

Uses (11)

Used by (5)