Supplementary Material for the Paper Verifying and Generalizing Simultaneous Critical Pairs (IWC 2026)

Formalization

The websites of the IsaFoR library have been produced with a slightly modified version of IsaFoR 3.8 (hg id 162127124070) using Isabelle 2025-2 and a corresponding version of the Archive of Formal Proofs.
All modifications will be part of the next release of IsaFoR.

• Definition 4
• Theorem 5
• Corollary 6 (Commutation)
• Corollary 6 (Confluence)
• Internal definition of rp (compute_rp in the formalization)
• Second defining equation of rp as in IWC paper
• Definition of rp_root
• Definition of rp_sub
• Theorem 8
• Definition of sim_cp_impl
• Soundness statement about sim_cp_impl
• Distinctness of sim_cp_impl

Experiments

• # 419
• # 463
• # 464