Technical Report with Proofs for A Full Picture in Conformance Checking: Efficiently Summarizing All Optimal Alignments

Repeated application of the reduction rules to δ is terminating. None of (R1-R3) increases the size of this set again. We prove local confluency for every pair of rules where the left sides overlap. We only inspect moves where there can be overlapping rules, i.e., (R2,R3) and (R2,R2). Canonicity follows from both propositions together with Newman's Lemma [1].