ParallelProofs.pair_facts: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend as ParallelProofs
Lines 142-157 of bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&start_line=142&end_line=157

import Base
import bendtorch-core@0.1.0.0/src/tensor/parallel.bend as Build

def pair_facts(~P: Data, ~A: Type, ~B: Type, ~cell: @+p: P -> @+position: Nat -> (A & B) -> Bool -> F32 & (A & B),
  +p: P, -start: (A & B), +count: Nat, +base: Nat, low: F32 & (A & B),
  -exact: {low == cell(p, base, start, Nat.is_lt(base, count)) : F32 & (A & B)},
  -keeps: Keeps(~P, ~A, ~B, ~cell, p, start)) ->
  Fact<TreeFacts(~P, ~A, ~B, ~cell, p, start, 1n, count, base, Build.pair(~P, ~A, ~B, ~cell, p, count, base, low))>:
  (x, s) = low
  (l, r) = s
  pair_join_facts(~P, ~A, ~B, ~cell, p, start, count, base, x, cell(p, Nat.add(1n, base), (l, r), Nat.is_lt(Nat.add(1n, base), count)),
    facts_cells(~P, ~A, ~B, ~cell, p, start, 0n, count, base, Build.leaf(~(A & B), (x, (l, r))),
      leaf_facts(~P, ~A, ~B, ~cell, p, start, count, base, (x, (l, r)), exact, keeps)),
    Equal.cong((A & B), F32 & (A & B), q => cell(p, Nat.add(1n, base), q, Nat.is_lt(Nat.add(1n, base), count)), (l, r), start,
      {\{Fact: q => q} : Fact<({Pair.snd(Array<F32>, (A & B), Build.leaf(~(A & B), (x, (l, r)))) == start : (A & B)})> ->
        {Pair.snd(Array<F32>, (A & B), Build.leaf(~(A & B), (x, (l, r)))) == start : (A & B)}}(
        facts_kept(~P, ~A, ~B, ~cell, p, start, 0n, count, base, Build.leaf(~(A & B), (x, (l, r))),
          leaf_facts(~P, ~A, ~B, ~cell, p, start, count, base, (x, (l, r)), exact, keeps)))),
    keeps)

Uses (19):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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=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.snd
  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/tensor/parallel.bend&name=leaf
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel.bend&name=pair
  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=Keeps
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=TreeFacts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=facts_cells
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=facts_kept
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=leaf_facts
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/tensor/parallel_proofs.bend&name=pair_join_facts