ReduceFiberProof.kept_after: 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 693-712 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=693&end_line=712

import Base
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape

# On a kept row, the blocks after the target's digit hold no position.
def kept_after(+f: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat, +digit: Nat,
  +after: {Nat.is_lt(Nat.div(target, left), digit) == True{} : Bool}, +bound: BoundBy<rest, left, stride>) ->
  {masked(Nat.mul(f, stride), Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) == Nil{} : List<&2, Nat>}:
  match f:
    case 0n:
      {==}
    case 1n+g:
      +rows : List<&2, Shape.Row> = Shape.Row{stride, left, right} <> rest
      +c = Nat.mul(digit, stride)
      %Equal.sym(List<&2, Nat>, masked(Nat.add(stride, Nat.mul(g, stride)), rows, target, base, c),
        List.append(&2, Nat, masked(stride, rows, target, base, c), masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))),
        masked_split(stride, Nat.mul(g, stride), rows, target, base, c)) :
        {_ == Nil{} : List<&2, Nat>}
      %Equal.sym(List<&2, Nat>, masked(stride, rows, target, base, c), Nil{},
        block_off(stride, left, right, rest, target, base, digit, Off{bound, gt_not_eq(digit, Nat.div(target, left), after)})) :
        {List.append(&2, Nat, _, masked(Nat.mul(g, stride), rows, target, base, Nat.add(c, stride))) == Nil{} : List<&2, Nat>}
      %next_cursor(digit, stride) :
        {masked(Nat.mul(g, stride), rows, target, base, _) == Nil{} : List<&2, Nat>}
      kept_after(g, stride, left, right, rest, target, base, 1n+digit, lt_succ_right(Nat.div(target, left), digit, after), bound)

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.mul
  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=OffMode
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=block_off
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=gt_not_eq
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=lt_succ_right
  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=masked_split
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=next_cursor
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=Row