In proving the graph minor theorem, Robertson and Seymour proved a stronger statement, namely that [the directed graph minor theorem][1] 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][2] and [here][3] 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
> 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.

  [1]: https://web.math.princeton.edu/~pds/papers/GM20/GM20.pdf
  [2]: https://pdfs.semanticscholar.org/cb07/9e02e28d07f9bf4ffc317f52dab68a02c62d.pdf
  [3]: https://pdfs.semanticscholar.org/4bad/6b436b1e25ff654d34466d05e1fa55162439.pdf