ReduceParallelProof.offset_shift: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend as ReduceParallelProof
Lines 355-375 of bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&start_line=355&end_line=375

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/index_proofs.bend as Index
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

# The one word that rows of span 1 reach from `base` sits `base` past the
# one they reach from 0.
def offset_shift(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +target: Nat, +base: Nat) ->
  {Reduce.single_offset(rows, extents, target, base) == Nat.add(base, Reduce.single_offset(rows, extents, target, 0n)) : Nat}:
  match rows extents:
    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others:
      +inner = Nat.mod(target, left)
      +step = Nat.mul(right, Nat.div(target, left))
      +below = Reduce.single_offset(rest, others, inner, 0n)
      Equal.trans(Nat, Reduce.single_offset(rest, others, inner, Nat.add(base, step)), Nat.add(Nat.add(base, step), below),
        Nat.add(base, Reduce.single_offset(rest, others, inner, step)),
        offset_shift(rest, others, inner, Nat.add(base, step)),
        Equal.trans(Nat, Nat.add(Nat.add(base, step), below), Nat.add(base, Nat.add(step, below)),
          Nat.add(base, Reduce.single_offset(rest, others, inner, step)),
          Equal.sym(Nat, Nat.add(base, Nat.add(step, below)), Nat.add(Nat.add(base, step), below), Index.add_assoc(base, step, below)),
          Equal.cong(Nat, Nat, x => Nat.add(base, x), Nat.add(step, below), Reduce.single_offset(rest, others, inner, step),
            Equal.sym(Nat, Reduce.single_offset(rest, others, inner, step), Nat.add(step, below), offset_shift(rest, others, inner, step)))))
    case Nil{} +extents:
      add_zero(base)
    case Shape.Row{+stride, +left, +right} <> +rest Nil{}:
      add_zero(base)

Uses (13):
  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=List
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=single_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/index_proofs.bend&name=add_assoc