Manuscript VII-E@1 · VII-E.tex · theorem · b713cf3c
Theorem: Retiming invariance
Prescribed kinematics and schedule dependence › Retiming fixed labelled channels · lines 770–786 · proof included or linked
VII-E@1#thm:retiming
All legal executions of an admissibly ordered labelled channel collection have the same total channel.
Proof. Incomparable channels have disjoint supports, so their extensions by identities commute. Any two linear extensions are connected by adjacent swaps of incomparable elements.
For completeness, compare two extensions at their first disagreement. Move the desired element leftwards in the first extension. Each intervening element is incomparable with it: either order relation would contradict one of the two extensions. Repeating this procedure makes the extensions equal. Every swap preserves the composed channel.