def chosen_reached

bendtorch-core@0.1.0.0 · src/autograd/backward_PROOF.bend:232

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

232def chosen_reached(+node: Backward.Node, +rest: List<&2, Backward.Node>, +below: Nat, +output: Nat, flag: Bool,
233  ih: {Laws.somes(Backward.pass(rest, below, output)) == Laws.reached(rest, below, output) : List<&2, Bool>}) ->
234  {Laws.somes(Backward.chosen(node, rest, below, unit => Backward.pass(rest, below, output), flag)) ==
235    Laws.reached_chosen(node, rest, below, unit => Laws.reached(rest, below, output), flag) : List<&2, Bool>}:
236  match flag:
237    case True{}:
238      %somes_nones(below) :
239        {Laws.somes(Backward.sweep(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)) ==
240          Laws.reach(node <> rest, True{} <> _, 1n+below) : List<&2, Bool>}
241      sweep_reach(node <> rest, Some{1.0} <> Backward.nones(below), 1n+below)
242    case False{}:
243      Equal.cong(List<&2, Bool>, List<&2, Bool>, xs => False{} <> xs,
244        Laws.somes(Backward.pass(rest, below, output)), Laws.reached(rest, below, output), ih)