TensorChainPROOF.gathered: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend as TensorChainPROOF
Lines 27-43 of bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&start_line=27&end_line=43

import Base
import bendtorch-core@0.1.0.0/src/autograd/gradient.bend as Gradient
import bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend as Laws

# With no entry left, the pull side gathers exactly the pending slots.
def gathered(pending: List<&1, Gradient.Slot>, +count: Nat, -slots: List<&1, Gradient.Slot>, -log: Laws.Log(),
  pulls: Pulls(pending, slots, count, log)) -> {Laws.gather(slots, count, log) == Done{pending} : Laws.Slots()}:
  match pending count:
    case Nil{} count:
      %Equal.sym(List<&1, Gradient.Slot>, slots, Nil{}, pulls) : {Laws.gather(_, count, log) == Done{Nil{}} : Laws.Slots()}
      {==}
    case Con{x, rest} 0n:
      %Equal.sym(List<&1, Gradient.Slot>, slots, x <> rest, pulls) : {Laws.gather(_, 0n, log) == Done{x <> rest} : Laws.Slots()}
      {==}
    case Con{x, rest} 1n+below:
      Cell{w, older, left, at, took, tail} = pulls
      %Equal.sym(List<&1, Gradient.Slot>, slots, w <> older, at) : {Laws.gather(_, 1n+below, log) == Done{x <> rest} : Laws.Slots()}
      %Equal.sym(Laws.Taken(), Laws.take(log, below, w), (Done{x}, left), took) :
        {Laws.gather_step(_, more => Laws.gather(older, below, more)) == Done{x <> rest} : Laws.Slots()}
      Equal.cong(Laws.Slots(), Laws.Slots(), result => Backward.prepend(Gradient.Slot, x, result),
        Laws.gather(older, below, left), Done{rest}, gathered(rest, below, older, left, tail))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=Result
  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/gradient.bend&name=Slot
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_backward.bend&name=prepend
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=Log
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=Slots
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=Taken
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=gather
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=gather_step
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_LAWS.bend&name=take
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=Cell
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/tensor_chain_PROOF.bend&name=Pulls