BackwardPROOF.chosen_reached: def of bendtorch-core@0.1.0.0
Import: import bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend as BackwardPROOF
Lines 232-244 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=232&end_line=244

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 chosen_reached(+node: Backward.Node, +rest: List<&2, Backward.Node>, +below: Nat, +output: Nat, flag: Bool,
  ih: {Laws.somes(Backward.pass(rest, below, output)) == Laws.reached(rest, below, output) : List<&2, Bool>}) ->
  {Laws.somes(Backward.chosen(node, rest, below, unit => Backward.pass(rest, below, output), flag)) ==
    Laws.reached_chosen(node, rest, below, unit => Laws.reached(rest, below, output), flag) : List<&2, Bool>}:
  match flag:
    case True{}:
      %somes_nones(below) :
        {Laws.somes(Backward.sweep(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)) ==
          Laws.reach(node <> rest, True{} <> _, 1n+below) : List<&2, Bool>}
      sweep_reach(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)
    case False{}:
      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs,
        Laws.somes(Backward.pass(rest, below, output)), Laws.reached(rest, below, output), ih)

Uses (16):
  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=List
  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=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=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_LAWS.bend&name=reach
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reached
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_LAWS.bend&name=reached_chosen
  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_nones
  https://jend.leeeet.dev/definition.txt?path=bendtorch-core@0.1.0.0/src/autograd/backward_PROOF.bend&name=sweep_reach