law shrn_lt_words

lawful-words@0.1.0.0 · LAWS.bend:239

import Base

239# An index below 2^k * w words-worth has its word index below w.
240law shrn_lt_words:
241  for i: U32
242  for w: U32
243  for k: Nat
244  for h: {Nat.is_lt(U32.to_nat(i), Nat.mul(Nat.pow(2n, k), U32.to_nat(w))) == True{} : Bool}
245  {U32.is_lt(U32.shrn(i, k), w) == True{} : Bool}