def um.e

bend-osdev-u32@0.1.0.0 · PROOF.bend:1449

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

1449def um.e(+n: Nat, +a: Word(n), +b: Word(n)) -> {Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, um.k(n, n, a, b, Word.zero(n)))) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}:
1450  Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, um.k(n, n, a, b, Word.zero(n)))), Nat.add(0n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, um.k(n, n, a, b, Word.zero(n)))), Nat.add(Word.to_nat(n, Word.zero(n)), Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Nat.add(0n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), um.go(n, n, a, b, Word.zero(n)), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))), Word.to_nat(n, Word.zero(n)), 0n, Laws.word_zero_value(n))), {==})