ReduceFiberProof.visited_base: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend as ReduceFiberProof
Lines 606-640 of bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&start_line=606&end_line=640

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

def visited_base(+rows: List<&2, Shape.Row>, +extents: List<&2, Nat>, +fuel: Nat, +target: Nat, +base: Nat, +digit: Nat) ->
  {visited(rows, extents, fuel, target, base, digit) == shift(base, visited(rows, extents, fuel, target, 0n, digit)) : List<&2, Nat>}:
  match rows extents fuel:
    case Nil{} _ _:
      %Equal.sym(Nat, Nat.add(base, 0n), base, Broadcast.add_zero(base)) : {[base] == [_] : List<&2, Nat>}
      {==}
    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 0n:
      {==}
    case Shape.Row{+stride, +left, +right} <> +rest +extent <> +others 1n+remaining:
      +inner = Nat.mod(target, left)
      +offset = Nat.mul(right, digit)
      +span = Reduce.first_span(rest, others)
      +first = Reduce.first_digit(rest, inner)
      +low = visited(rest, others, span, inner, 0n, first)
      +high = visited(rows, extents, remaining, target, 0n, 1n+digit)
      %Equal.sym(List<&2, Nat>, visited(rest, others, span, inner, Nat.add(base, offset), first), shift(Nat.add(base, offset), low),
        visited_base(rest, others, span, inner, Nat.add(base, offset), first)) :
        {List.append(&2, Nat, _, visited(rows, extents, remaining, target, base, 1n+digit)) ==
          shift(base, List.append(&2, Nat, visited(rest, others, span, inner, offset, first), high)) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, visited(rows, extents, remaining, target, base, 1n+digit), shift(base, high),
        visited_base(rows, extents, remaining, target, base, 1n+digit)) :
        {List.append(&2, Nat, shift(Nat.add(base, offset), low), _) ==
          shift(base, List.append(&2, Nat, visited(rest, others, span, inner, offset, first), high)) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, visited(rest, others, span, inner, offset, first), shift(offset, low),
        visited_base(rest, others, span, inner, offset, first)) :
        {List.append(&2, Nat, shift(Nat.add(base, offset), low), shift(base, high)) ==
          shift(base, List.append(&2, Nat, _, high)) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, shift(base, List.append(&2, Nat, shift(offset, low), high)),
        List.append(&2, Nat, shift(base, shift(offset, low)), shift(base, high)), shift_append(base, shift(offset, low), high)) :
        {List.append(&2, Nat, shift(Nat.add(base, offset), low), shift(base, high)) == _ : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, shift(base, shift(offset, low)), shift(Nat.add(base, offset), low), shift_shift(base, offset, low)) :
        {List.append(&2, Nat, shift(Nat.add(base, offset), low), shift(base, high)) == List.append(&2, Nat, _, shift(base, high)) : List<&2, Nat>}
      {==}
    case Shape.Row{+stride, +left, +right} <> +rest Nil{} _:
      {==}

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  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.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=first_digit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=first_span
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=shift_append
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=shift_shift
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=visited
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/broadcast_proofs.bend&name=add_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row