WQO dichotomy conjecture — proof of a special case, part 2

The conjecture claims that there exists a simple criterion for decidability
for Petri nets with homogeneous data.
We prove a special case of this conjecture for data being 2-edge-coloured graphs.
I will outline the overall structure of the proof and sketch some of its interesting parts.