Graph-Minor Theorem for Directed Graphs? Suppose that $\vec{G}$ is a directed graph and that $G$ is the undirected graph obtained from $\vec{G}$ by forgetting the direction on each edge. Define $\vec{H}$ to be a minor of $\vec{G}$ if $H$ is a minor of $G$ as undirected graphs and direction on the edges of $\vec{H}$ are the same as the corresponding edges in $\vec{G}$. 
Does the Robertson-Seymour Theorem hold for directed graphs (where the above definition of minor is used and our graphs are allowed to have loops and multiple edges)?

I think the answer is yes, see 10.5 in Neil Robertson and Paul D. Seymour. Graph minors. xx. wagner’s conjecture. Journal of Combinatorial Theory, 92:325–357, 2004. and the preceding section:

As a corollary, we deduce the following form of Wagner’s conjecture for directed graphs (which immediately implies the standard form of the conjecture for undirected graphs). A directed graph is a minor of another if the first can be obtained from a subgraph of the second by contracting edges.
10.5  Let $G_i$ ($i = 1,2,\ldots$) be a countable sequence of directed graphs. Then there exist $j > i \geq 1$ such that $G_i$ is isomorphic to a minor of $G_j$.

I haven't tried to understand the proof and I don't plan to try anytime soon. But I'm pretty sure that the used definition of digraph minor is identical to your definition, and that the statement is exactly the theorem you asked for.
