law to_nat_shrn_lt

lawful-words@0.1.0.0 · LAWS.bend:221

import Base

221# A right shift by k leaves a number below 2^(32-k) (below 1 from k = 32 up).
222law to_nat_shrn_lt:
223  for a: U32
224  for k: Nat
225  {Nat.is_lt(U32.to_nat(U32.shrn(a, k)), Nat.pow(2n, Nat.sub(32n, k))) == True{} : Bool}