ReduceFiberProof.kept_row: 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 790-817 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=790&end_line=817

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend as Nats
import bendtorch-core@0.1.0.0/src/storage/arith.bend as Arith
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

# A kept row walks the one digit the target names there.
def kept_row(+size: Nat, +stride: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
  +target: Nat, +base: Nat, +inside: {Nat.is_lt(target, Nat.mul(extent, size)) == True{} : Bool},
  +walk: RestWalk(rest, others, Nat.mod(target, size), stride), +bound: BoundBy<rest, size, stride>) ->
  {masked(Nat.mul(extent, stride), Shape.Row{stride, size, right} <> rest, target, base, 0n) ==
    visited(Shape.Row{stride, size, right} <> rest, extent <> others, Reduce.span(size, extent), target, base, Nat.div(target, size)) :
    List<&2, Nat>}:
  match size:
    case 0n:
      Empty.absurd({masked(Nat.mul(extent, stride), Shape.Row{stride, 0n, right} <> rest, target, base, 0n) ==
        visited(Shape.Row{stride, 0n, right} <> rest, extent <> others, Reduce.span(0n, extent), target, base, Nat.div(target, 0n)) :
        List<&2, Nat>},
        Arith.lt_zero(target,
          %Nats.mul_zero_right(extent) : {Nat.is_lt(target, _) == True{} : Bool}
          inside))
    case 1n+l:
      +dt = Nat.div(target, 1n+l)
      +tr = Nat.mod(target, 1n+l)
      +w = visited(rest, others, Reduce.first_span(rest, others), tr, Nat.add(base, Nat.mul(right, dt)), Reduce.first_digit(rest, tr))
      %Equal.sym(List<&2, Nat>, masked(Nat.mul(extent, stride), Shape.Row{stride, 1n+l, right} <> rest, target, base, 0n),
        masked(stride, rest, tr, Nat.add(base, Nat.mul(right, dt)), 0n),
        kept_hit(extent, stride, 1n+l, right, rest, target, base, 0n, Arith.le_zero(dt),
          div_below(target, extent, 1n+l, inside), decompose(target, 1n+l, {==}), bound)) :
        {_ == List.append(&2, Nat, w, Nil{}) : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, masked(stride, rest, tr, Nat.add(base, Nat.mul(right, dt)), 0n), w,
        rest_at(rest, others, tr, stride, walk, Nat.add(base, Nat.mul(right, dt)))) :
        {_ == List.append(&2, Nat, w, Nil{}) : List<&2, Nat>}
      Equal.sym(List<&2, Nat>, List.append(&2, Nat, w, Nil{}), w, append_nil(w))

Uses (27):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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.div
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_lt
  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.bend&name=span
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=BoundBy
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=RestWalk
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=append_nil
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=decompose
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=div_below
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept_hit
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=masked
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=rest_at
  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/core.bend&name=Row
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/nat_proofs.bend&name=mul_zero_right
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=le_zero
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/arith.bend&name=lt_zero