Supplementary Material

This is the web page for the supplementary material of the CPP 2025 paper: An Isabelle Formalization of Co-rewrite Pairs for Non-reachability in Term Rewriting.

Formalization

The supplementary material has been generated from IsaFoR/CeTA version 3.3 using Isabelle 2024. Most of the formalization is accessible directly via the icon links within the paper. For convenience, we here provide the links as well.

• Theorem 3.2
• Theorem 3.3
• Lemma 4.1
• Theorem 4.3
• Corollary 4.4
• Theorem 5.1
• Proposition 5.3
• Term_Order_Impl.thy
• WPO_Impl.thy

Experiments

The experiments are described in more detail here.

IsaFoR/CeTA

In order to obtain IsaFoR/CeTA version 3.3 we refer to the download on the IsaFoR/CeTA website.