law u32_mul_low

bend-osdev-u32@0.1.0.0 · LAWS.bend:485

import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U

485law u32_mul_low:
486  for +a: U32
487  for +b: U32
488  {U32.to_nat(U32.mul(a, b)) == U.U32Nat.low(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))) : Nat}