BackwardPROOF.sweep_reach: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 207-223 of bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&start_line=207&end_line=223

import Base
import bendtorch-core@0.1.0.0/src/autograd/backward.bend as Backward
import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as Laws

def sweep_reach(nodes: List<&2, Backward.Node>, gradients: List<&2, Maybe<&2, F32>>, +count: Nat) ->
  {Laws.somes(Backward.sweep(nodes, gradients, count)) == Laws.reach(nodes, Laws.somes(gradients), count) : List<&2, Bool>}:
  match nodes gradients count:
    case Nil{} gradients count:
      {==}
    case Con{node, rest} Nil{} count:
      {==}
    case Con{node, rest} Con{gradient, pending} 0n:
      {==}
    case Con{+node, rest} Con{+gradient, +pending} 1n+below:
      %somes_contribute(node, gradient, below, pending) :
        {Maybe.is_some(&2, F32, gradient) <> Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)) ==
          Maybe.is_some(&2, F32, gradient) <> Laws.reach(rest, _, below) : List<&2, Bool>}
      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => Maybe.is_some(&2, F32, gradient) <> xs,
        Laws.somes(Backward.sweep(rest, Backward.contribute(node, gradient, below, pending), below)),
        Laws.reach(rest, Laws.somes(Backward.contribute(node, gradient, below, pending)), below),
        sweep_reach(rest, Backward.contribute(node, gradient, below, pending), below))

Uses (13):
  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=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe.is_some
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=Node
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=contribute
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=sweep
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reach
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=somes
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=somes_contribute