def unbound_ill_formed

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

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

483def unbound_ill_formed(+newer: List<&2, Backward.Entry>, +entry: Backward.Entry, +rest: List<&2, Backward.Entry>,
484  +unbound: {Laws.bounded(Laws.targets(Laws.entry_node(entry)), List.length(&2, Backward.Entry, rest)) == False{} : Bool}) ->
485  {Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, newer, entry <> rest))) == False{} : Bool}:
486  match newer:
487    case Nil{}:
488      head_ill_formed(entry, rest, unbound)
489    case Con{Backward.Entry{node, value, slot}, tail}:
490      %Equal.sym(Bool, Laws.well_formed(Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest))), False{},
491        unbound_ill_formed(tail, entry, rest, unbound)) :
492        {Bool.and(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest)))), _) ==
493          False{} : Bool}
494      and_false(Laws.bounded(Laws.targets(node), List.length(&2, Backward.Node, Backward.nodes(List.append(&2, Backward.Entry, tail, entry <> rest)))))