Supplementary Material

for the CPP 2025 paper "Formalizing Simultaneous Critical Pairs for Confluence of Left-Linear Rewrite Systems".

Formalization

The formalization described in the paper builds on IsaFoR/CeTA version 3.2 using Isabelle 2024.

We provide HTML presentations of the IsaFoR source code. The following theory files might be of interest.

Session`CR`

Okui_Criterion.thy: Definition of simultaneous critical pairs and proof of Okui's criterion
Okui_subsumes_DC.thy: Proof that Okui's criterion subsumes development closedness

Session `Proof_Terms`

Proof_Terms.thy Definition and basic results about proof terms
Residual_Join_Deletion.thy Operations on proof terms
Orthogonal_PT.thy Orthogonal proof terms and their properties
Labels_and_Overlaps.thy Labeling of the source of proof terms, used to determine overlap
Redex_Patterns.thy Properties of redex patterns contained in proof terms

Session`TRS`

Unification_More.thy: Unification of linear terms

Proof_Terms session graph

session graph for Proof_Terms