law word_mul_low

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

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

466law word_mul_low:
467  for +n: Nat
468  for +a: Word(n)
469  for +b: Word(n)
470  {Word.to_nat(n, Word.mul(n, a, b)) == U.U32Nat.low(n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}