ParallelLAWS.parallel_build_balanced: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_LAWS.bend as ParallelLAWS
Lines 14-29 of bendtorch-core@0.1.0.0/src/tensor/parallel_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_LAWS.bend&start_line=14&end_line=29

import Base
import bendtorch-core@0.1.0.0/src/storage/model.bend as Model
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Parallel

# For every split, the parallel build is a balanced tree of its depth.
law parallel_build_balanced:
  for ~Q: Data
  for ~P: Data
  for ~A: Type
  for ~B: Type
  for ~prepare: @+q: Q -> P
  for ~split: A & B -> (A & B) & (A & B)
  for ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B)
  for +q: Q
  for +depth: Nat
  for +splits: Nat
  for +count: Nat
  for +base: Nat
  for state: (A & B)
  Model.Balanced(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state))

Uses (7):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=balanced
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=build