law shl2

lawful-bytes@0.1.1.0 · proof_fast_find.bend:470

import Base

470law shl2:
471  for +wi: U32
472  for +d: Nat
473  for +hd: {Nat.is_le(d, 29n) == True{} : Bool}
474  for +hx: {Nat.is_le(Nat.mul(U32.to_nat(wi), 4n), Nat.mul(4n, Nat.pow(2n, d))) == True{} : Bool}
475  {U32.to_nat((wi << 2n : U32)) == Nat.mul(U32.to_nat(wi), 4n) : Nat}