New and Formalized Proofs for Right-Forward Closures and Core Matrix Interpretations

Example Certificates

• Certificate for Example 21. It was manually translated from an MnM-proof to CeTA's format.
• Certificate for Example 23. It was manually translated from a matchbox-proof to CeTA's format.
• Certificate for Example 25. A trivial TRS has been added. This example mainly illustrated that negative numbers may appear in interpretations, because of the decision procedures in Lemma 24.

Verifying the certificates can be done by CeTA version 3.8.

Formalization

Below we provide links that connect the results from the paper to their formalized counterparts. The HTML-pages have been generated using Isabelle 2025-2, The Archive of Formal Proofs, and IsaFoR version 3.8.

Section 3

• Definition of RFC(R)
• Lemma 8
• Lemma 9 in slightly different form
• Lemma 10
• Lemma 11
• Gramlich's result on equivalence of termination and innermost termination for locally confluenct overlay TRSs
• Theorem 3 (right-linear TRSs)
• Theorem 3 (locally confluent overlay TRSs)

Section 4

• Definition of core
• Lemma 16 (E_I)
• Lemma 16 (M_I, important inclusion)
• Lemma 16 (M_I, inclusion with change of δ)
• Theorem 18 (E_I)
• Theorem 18 (M_I)
• Theorem 18 with sufficient criteria of Theorem 19 (E_I)
• Theorem 18 with sufficient criteria of Theorem 19 (M_I)
• Lemma 22
• Lemma 24
• Lemma 27
• We did neither formalize Lemma 26 nor Theorem 28.