ReduceFiberProof.kept_hit: 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 770-788 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=770&end_line=788

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

# On a kept row, the blocks from `digit` that cover the target's digit hold
# exactly the rows below at the target's remainder.
def kept_hit(+f: Nat, +stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +target: Nat, +base: Nat, +digit: Nat,
  +from: {Nat.is_le(digit, Nat.div(target, left)) == True{} : Bool},
  +until: {Nat.is_lt(Nat.div(target, left), Nat.add(digit, f)) == True{} : Bool},
  +given: Decomposed<target, left>, +bound: BoundBy<rest, left, stride>) ->
  {masked(Nat.mul(f, stride), Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) ==
    masked(stride, rest, Nat.mod(target, left), Nat.add(base, Nat.mul(right, Nat.div(target, left))), 0n) : List<&2, Nat>}:
  match f:
    case 0n:
      Empty.absurd({masked(0n, Shape.Row{stride, left, right} <> rest, target, base, Nat.mul(digit, stride)) ==
        masked(stride, rest, Nat.mod(target, left), Nat.add(base, Nat.mul(right, Nat.div(target, left))), 0n) : List<&2, Nat>},
        le_lt_absurd(digit, Nat.div(target, left), from,
          %Broadcast.add_zero(digit) : {Nat.is_lt(Nat.div(target, left), _) == True{} : Bool}
          until))
    case 1n+g:
      kept_hit_step(g, stride, left, right, rest, target, base, digit, Shape.bool_case(Nat.is_eq(digit, Nat.div(target, left))),
        from, until, given, bound,
        next => from => until => kept_hit(g, stride, left, right, rest, target, base, next, from, until, given, bound))

Uses (19):
  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=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.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le
  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_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=Decomposed
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=kept_hit_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_fiber_proof.bend&name=le_lt_absurd
  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/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
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/shape/core.bend&name=bool_case