BackwardLAWS.seed_selected_output: law of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend as BackwardLAWS
Lines 247-259 of bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend: https://jend.leeeet.dev/read.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&start_line=247&end_line=259

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

# The seed is the selected output (C1). For any graph, the nodes newer than
# the output get None, the output gets exactly 1.0, and the older nodes get
# what the sweep sends from the output's VJP, whatever the newer nodes are.
law seed_selected_output:
  for +newer: List<&2, Backward.Node>
  for +node: Backward.Node
  for +rest: List<&2, Backward.Node>
  {Backward.pass(List.append(&2, Backward.Node, newer, node <> rest),
      List.length(&2, Backward.Node, List.append(&2, Backward.Node, newer, node <> rest)), List.length(&2, Backward.Node, rest)) ==
    List.append(&2, Maybe<&2, F32>, Backward.nones(List.length(&2, Backward.Node, newer)),
      Some{1.0} <> Backward.sweep(rest,
        Backward.contribute(node, Some{1.0}, List.length(&2, Backward.Node, rest), Backward.nones(List.length(&2, Backward.Node, rest))),
        List.length(&2, Backward.Node, rest))) : List<&2, Maybe<&2, F32>>}

Uses (14):
  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=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=chosen
  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=nones
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward.bend&name=pass
  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_PROOF.bend&name=append_ne
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=eq_refl