ElementwiseWalkProof.go_total: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend as ElementwiseWalkProof
Lines 28-59 of bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&start_line=28&end_line=59

import Base
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith

# The division loop keeps quotient * (1 + bp) + remainder + what is left to
# count fixed, as long as the remainder and the countdown add up to bp.
def go_total(+n: Nat, +m: Nat, +d: Nat, +r: Nat, +bp: Nat, +fits: {Nat.add(m, r) == bp : Nat}) ->
  {Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(n, m, d, r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(n, m, d, r))) ==
    Nat.add(Nat.add(Nat.mul(d, 1n+bp), r), n) : Nat}:
  match n m:
    case 0n m:
      add_zero_left(Nat.add(Nat.mul(d, 1n+bp), r))
    case 1n+np 0n:
      +total = Nat.mul(d, 1n+bp)
      Equal.trans(Nat,
        Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, r, 1n+d, 0n))),
        1n+Nat.add(Nat.add(Nat.add(bp, total), 0n), np),
        Nat.add(Nat.add(total, r), 1n+np),
        go_total(np, r, 1n+d, 0n, bp, Equal.trans(Nat, Nat.add(r, 0n), r, bp, Equal.sym(Nat, r, Nat.add(r, 0n), add_zero_left(r)), fits)),
        Equal.trans(Nat, 1n+Nat.add(Nat.add(Nat.add(bp, total), 0n), np), 1n+Nat.add(Nat.add(total, r), np), Nat.add(Nat.add(total, r), 1n+np),
          Equal.cong(Nat, Nat, x => 1n+Nat.add(x, np), Nat.add(Nat.add(bp, total), 0n), Nat.add(total, r),
            Equal.trans(Nat, Nat.add(Nat.add(bp, total), 0n), Nat.add(bp, total), Nat.add(total, r),
              Equal.sym(Nat, Nat.add(bp, total), Nat.add(Nat.add(bp, total), 0n), add_zero_left(Nat.add(bp, total))),
              Equal.trans(Nat, Nat.add(bp, total), Nat.add(total, bp), Nat.add(total, r), add_comm(bp, total),
                Equal.cong(Nat, Nat, x => Nat.add(total, x), bp, r, Equal.sym(Nat, r, bp, fits))))),
          Equal.sym(Nat, Nat.add(Nat.add(total, r), 1n+np), 1n+Nat.add(Nat.add(total, r), np), Arith.add_succ(Nat.add(total, r), np))))
    case 1n+np 1n+mp:
      +total = Nat.mul(d, 1n+bp)
      Equal.trans(Nat,
        Nat.add(Nat.mul(Pair.fst(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r)), 1n+bp), Pair.snd(Nat, Nat, Nat.divmod.go(np, mp, d, 1n+r))),
        Nat.add(Nat.add(total, 1n+r), np),
        Nat.add(Nat.add(total, r), 1n+np),
        go_total(np, mp, d, 1n+r, bp, Equal.trans(Nat, Nat.add(mp, 1n+r), 1n+Nat.add(mp, r), bp, Arith.add_succ(mp, r), fits)),
        Equal.trans(Nat, Nat.add(Nat.add(total, 1n+r), np), 1n+Nat.add(Nat.add(total, r), np), Nat.add(Nat.add(total, r), 1n+np),
          Equal.cong(Nat, Nat, x => Nat.add(x, np), Nat.add(total, 1n+r), 1n+Nat.add(total, r), Arith.add_succ(total, r)),
          Equal.sym(Nat, Nat.add(Nat.add(total, r), 1n+np), 1n+Nat.add(Nat.add(total, r), np), Arith.add_succ(Nat.add(total, r), np))))

Uses (12):
  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.sym
  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.divmod.go
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=add_succ
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=add_comm
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_walk_proof.bend&name=add_zero_left