law wmul_go

lawful-words@0.1.0.0 · proof_word.bend:707

import Base

707law wmul_go:
708  for +n: Nat
709  for +m: Nat
710  for +a: Word(m)
711  for +b: Word(n)
712  for +acc: Word(n)
713  {Word.to_nat(n, Word.mul.go(n, m, a, b, acc))
714    == Nat.mod(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))), Nat.pow(2n, n)) : Nat}