Corollary: Compositional diamonds imply schedule independence

Suppose swapping independent enabled operations preserves their joint record law and leaves equivalent residual configurations for all subsequent operations. All schedules of a fixed finite history then have the same joint record law.

Proof. Apply Lemma lem:interchange to the complete computation. The residual condition makes each interchange valid in context.