ReduceParallelProof.strided_fiber: 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 517-528 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=517&end_line=528

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as Generic
import bendtorch-core@0.1.0.0/src/shape/core.bend as Shape
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

# The strided loop of such a row is its fiber.
def strided_fiber(+stride: Nat, +left: Nat, +right: Nat, +rest: List<&2, Shape.Row>, +extent: Nat, +others: List<&2, Nat>,
  +single: {Reduce.single_rows(rest, others) == True{} : Bool}, fuel: Nat, +target: Nat, +base: Nat, +digit: Nat, +accumulator: F32,
  array: Array<F32>) ->
  Generic.Fact<{Reduce.strided(fuel, right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n), accumulator, array) ==
    Reduce.fiber(Shape.Row{stride, left, right} <> rest, extent <> others, fuel, target, base, digit, accumulator, array) : F32 & Array<F32>}>:
  match fuel:
    case 0n:
      Generic.Fact{{==}}
    case 1n+remaining:
      run_fiber(stride, left, right, rest, extent, others, single, remaining, target, base, digit, accumulator, array,
        Array.get(F32, array, U32.from_nat(Reduce.strided_offset(right, base, digit, Reduce.single_offset(rest, others, Nat.mod(target, left), 0n)))), {==})

Uses (17):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array.get
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  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.mod
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=fiber
  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.bend&name=single_rows
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=strided
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=strided_offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=run_fiber
  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/tensor/parallel_proofs.bend&name=Fact