PROOF.um.go: def of bend-osdev-u32@0.1.0.0
Import: import bend-osdev-u32@0.1.0.0/PROOF.bend as PROOF
Lines 1438-1447 of bend-osdev-u32@0.1.0.0/PROOF.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&start_line=1438&end_line=1447

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

def um.go(+n: Nat, m: Nat, a: Word(m), +b: Word(n), +acc: Word(n)) -> {Nat.add(Word.to_nat(n, Word.mul.go(n, m, a, b, acc)), U.U32Nat.dbl(n, um.k(n, m, a, b, acc))) == Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(m, a), Word.to_nat(n, b))) : Nat}:
  match m:
    case 0n:
      ur.r20(Word.to_nat(n, acc), n, Word.to_nat(n, b))
    case 1n+ +mp:
      match a:
        case WCon{False{}, +at}:
          Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Nat.add(Word.to_nat(n, acc), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), acc), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), acc))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), Nat.add(Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), ur.r14(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), n, um.k(n, mp, at, Word.shl(n, b), acc), Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))), Equal.cong(Nat, Nat, zz => Nat.add(zz, U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))), Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), acc)), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), acc))), Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), um.go(n, mp, at, Word.shl(n, b), acc))), ur.r15(Word.to_nat(n, acc), Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)), n, U.U32Nat.bit(un.top(n, b)))), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(n, acc), Nat.mul(Word.to_nat(mp, at), zz)), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))), Nat.double(Word.to_nat(n, b)), un.shlv(n, b))), Equal.cong(Nat, Nat, zz => Nat.add(Word.to_nat(n, acc), zz), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b))), Nat.mul(Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b)), ur.r16(Word.to_nat(mp, at), Word.to_nat(n, b))))
        case WCon{True{}, +at}:
          Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Nat.add(Word.to_nat(n, acc), Nat.mul(1n+Nat.double(Word.to_nat(mp, at)), Word.to_nat(n, b))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.double(Word.to_nat(n, b)))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))))), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))))), Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Equal.trans(Nat, Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, Nat.add(um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), Nat.add(U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))))))), Nat.add(Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), ur.r17(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), n, um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)), U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b))), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.add(U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc)))), U.U32Nat.dbl(n, Nat.mul(Word.to_nat(mp, at), U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, Word.mul.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b))), U.U32Nat.dbl(n, um.k(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)))), Nat.add(Word.to_nat(n, Word.add(n, acc, b)), Nat.mul(Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)))), um.go(n, mp, at, Word.shl(n, b), Word.add(n, acc, b)))), ur.r18(Word.to_nat(n, Word.add(n, acc, b)), Word.to_nat(mp, at), Word.to_nat(n, Word.shl(n, b)), n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))), U.U32Nat.bit(un.top(n, b)))), Equal.cong(Nat, Nat, zz => Nat.add(zz, Nat.mul(Word.to_nat(mp, at), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))))), Nat.add(Word.to_nat(n, Word.add(n, acc, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, acc, b), acc))))), Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Laws.word_add_wrap(n, acc, b))), Equal.cong(Nat, Nat, zz => Nat.add(Nat.add(Word.to_nat(n, acc), Word.to_nat(n, b)), Nat.mul(Word.to_nat(mp, at), zz)), Nat.add(Word.to_nat(n, Word.shl(n, b)), U.U32Nat.dbl(n, U.U32Nat.bit(un.top(n, b)))), Nat.double(Word.to_nat(n, b)), un.shlv(n, b))), ur.r19(Word.to_nat(n, acc), Word.to_nat(n, b), Word.to_nat(mp, at)))

Uses (28):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.mul.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shl
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_add_wrap
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=um.k
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.shlv
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=un.top
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r14
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r15
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r16
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r17
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r18
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r19
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/PROOF.bend&name=ur.r20
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.bit
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/u32.bend&name=U32Nat.dbl