law word_to_nat_lt

bend-kit-lemmas@0.1.1.0 · lemmas.bend:162

import bend-kit-lemmas@0.1.1.0/lemmas.bend as Lemmas

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

162# A word of n bits has a value below 2^n.
163law word_to_nat_lt:
164  for n: Nat
165  for w: Word(n)
166  MNat.lt(Word.to_nat(n, w), pow2(n))

Uses (9)

Used by (3)