ParallelLAWS.parallel_build_sequential: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_LAWS.bend as ParallelLAWS
Lines 57-79 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=57&end_line=79

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

# Under the same two facts, the parallel build and the one-thread build
# (no split) hold the same F32 in every slot, so no output word depends on
# the split or on the thread count.
law parallel_build_sequential:
  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)
  for keeps: @+position: Nat -> @inside: Bool -> {Pair.snd(F32, (A & B), cell(prepare(q), position, state, inside)) == state : (A & B)}
  for first: {Pair.fst((A & B), (A & B), split(state)) == state : (A & B)}
  for second: {Pair.snd((A & B), (A & B), split(state)) == state : (A & B)}
  Holds<@+path: Model.Path(depth) ->
    {Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, splits, count, base, state), path) ==
      Model.observe(F32, depth, Parallel.build(~Q, ~P, ~A, ~B, ~prepare, ~split, ~cell, q, depth, 0n, count, base, state), path) : Maybe<&2, F32>}>

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=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=F32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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.is_lt
  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=Pair.snd
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=Path
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=observe
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/storage/model.bend&name=offset
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=build
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_LAWS.bend&name=Holds
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=Fact
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=build_cells