ReduceParallelProof.next_run: 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 296-316 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=296&end_line=316

import Base
import bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend as Parallel
import bendtorch-core@0.1.0.0/src/autograd/reduce.bend as Reduce

def next_run(+d: Nat, -A: Array<F32>, -low: List<&2, Nat>, -high: List<&2, Nat>, -accumulator: F32,
  -rec: F32 -> Array<F32> -> F32 & Array<F32>, pair: F32 & Array<F32>,
  -first: Parallel.Fact<FiberRun<d, A, low, accumulator, pair>>,
  -next: @value: F32 -> @array: Array<F32> -> @-same: {array == A : Array<F32>} -> Parallel.Fact<FiberRun<d, A, high, value, rec(value, array)>>) ->
  Parallel.Fact<FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, Reduce.walk_next(rec, pair)>>:
  (value, array) = pair
  Parallel.Fact{{\{FiberRun: words => seen => total => kept =>
    {\{FiberRun: rest => more => after => back =>
      FiberRun{List.append(&2, F32, words, rest),
        {\{Parallel.Fact: p => p} : Parallel.Fact<Obs(d, A, List.append(&2, Nat, low, high), List.append(&2, F32, words, rest))> ->
          Obs(d, A, List.append(&2, Nat, low, high), List.append(&2, F32, words, rest))}(obs_append(d, A, low, words, high, rest, seen, more)),
        %Equal.sym(F32, fsum(List.append(&2, F32, words, rest), accumulator), fsum(rest, fsum(words, accumulator)),
          fsum_append(words, rest, accumulator)) : {Pair.fst(F32, Array<F32>, rec(value, array)) == _ : F32}
        %total : {Pair.fst(F32, Array<F32>, rec(value, array)) == fsum(rest, _) : F32}
        after,
        back}} :
      FiberRun<d, A, high, value, rec(value, array)> -> FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, rec(value, array)>}(
      {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, high, value, rec(value, array)>> -> FiberRun<d, A, high, value, rec(value, array)>}(
        next(value)(array)(kept)))} :
    FiberRun<d, A, low, accumulator, (value, array)> -> FiberRun<d, A, List.append(&2, Nat, low, high), accumulator, rec(value, array)>}(
    {\{Parallel.Fact: p => p} : Parallel.Fact<FiberRun<d, A, low, accumulator, (value, array)>> -> FiberRun<d, A, low, accumulator, (value, array)>}(first))}

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=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=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair.fst
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce.bend&name=walk_next
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=FiberRun
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=Obs
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=fsum
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=fsum_append
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/reduce_parallel_proof.bend&name=obs_append
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/elementwise_parallel_proof.bend&name=Fact