def pass_reached

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

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

246def pass_reached(nodes: List<&2, Backward.Node>, +count: Nat, +output: Nat) ->
247  {Laws.somes(Backward.pass(nodes, count, output)) == Laws.reached(nodes, count, output) : List<&2, Bool>}:
248  match nodes count:
249    case Nil{} count:
250      {==}
251    case Con{node, rest} 0n:
252      {==}
253    case Con{+node, +rest} 1n+below:
254      chosen_reached(node, rest, below, output, Nat.is_eq(below, output), pass_reached(rest, below, output))