# Proof of trace respecting shuffles

Proposition (Trace respects shuffles) For any shuffle s between traceable sorts, if:

=
then:
=

Proof. An induction on the number of incoming and outgoing edges of s. Throughout the proof, we shall use the previously established completeness and expressivity of acyclic graphs.

First, we consider the case when s has no outgoing edges, in which case it is the terminal graph and:

= |  | (Product)
= |  | (Naturality of terminal)
= |  | (Naturality of Tr)
= |  | (Hypothesis)
= |  | (Product)

Next, we consider the case when s has one incoming edge, so is of the form:
for which it suffices to show that if:
for all s1 and s2, =
then:
=
We proceed by induction on the number of traced edges. If there is one traced edge, then the result is immediate. For the inductive step, by the hypothesis we have:
for all s1 and s2, =
so by induction:
=
and similarly:
=
So:

= |  | (Naturality of Tr)
= |  | (Above)
= |  | (Hypothesis)
= |  | (Above)
= |  | (Naturality of Tr)

So:

= |  | (Trace respects product)
= |  | (Above)

Finally, we conside the case when s has more than one incoming edge, and so is of the form:
=
So:
=
and since permutations are isos:
=
So by induction:
=
and by induction again:
=
and so by dinaturality:
=

Back