In proving the graph minor theorem, Robertson and Seymour proved a stronger statement, namely that the directed graph minor theorem is true, using the definition

A directed graph is a minor of another if the first can be obtained from a subgraph of the second by contracting edges.

Since then, many more notions of a “directed graph minor” have arisen in various context (see here and here for examples and references). One of the goals in defining these notions is that the definition Robertson and Seymour gave doesn’t obviously capture the notion that if $G$ is a minor of $H$, then $G$ should be “simpler” than $H$.

I’m looking for references to proofs of the graph minor theorem for these more restrictive definitions of “graph minor.” I’m particularly interested in the following definition (Johnson et al., 2001):

A graph $G’$ is a butterfly minor of a directed graph $G$ if $G’$ can be obtained from $G$ by a sequence of the following local operations:

1. Deleting an edge (a, b);
2. Contracting an edge (a, b) where b has indegree 1;
3. Contracting an edge (a, b) where a has outdegree 1.

But other definitions would also interest me, especially if they’re amenable to analyzing computational graphs of circuits or ML devices (neural networks, Bayesian networks)