Proposition: Interchange of independent instructions

Two adjacent instructions acting on disjoint live factors, with no control or shared-resource dependency, may be interchanged without changing the complete channel, after the fixed output permutation.

This equality does not assert equality of their physical schedules or peak-storage ledgers.

Proof. The two maps have tensor forms ${\Phi }_A\otimes {\mathrm{id}}_B$ and ${\mathrm{id}}_A\otimes {\Psi }_B$, whose compositions agree. Classical outcomes are retained in their respective factors. Occupancy and timing are separate data and can differ between the two schedules.