Es sind mehrere Kriterien für kritische Paare bekannt, die den Zusammenfluss von linkslinearen Termumschreibsystemen garantieren. Die Korrektheit der meisten von ihnen wurde in einem Beweisassistenten formalisiert. Eine wichtige Ausnahme ist das Kriterium der Entwicklungsgeschlossenheit von van Oostrom. Der Papierbeweis stützt sich auf grafische Darstellungen und Intuition über überlappende Rexe und Deszendenten und hat sich bisher allen Formalisierungsversuchen entzogen. Wir präsentieren eine Formalisierung in dem Beweisassistenten Isabelle/HOL. Das Ergebnis wurde in den Zertifizierer CeTA integriert.
Link Für weitere Informationen.