law shrn_lt_words

lawful-words@0.1.0.0 · proof_u32.bend:1238

import Base

1238law shrn_lt_words:
1239  for +i: U32
1240  for +w: U32
1241  for +k: Nat
1242  for +h: {Nat.is_lt(U32.to_nat(i), Nat.mul(Nat.pow(2n, k), U32.to_nat(w))) == True{} : Bool}
1243  {U32.is_lt(U32.shrn(i, k), w) == True{} : Bool}