On Formalizing Decreasing Proof Orders
Y. Bitane · Utrecht University Repository (Utrecht University) · 2015
Confluence is an important property of term rewriting systems. Since any algorithm can be modelled as such, the decreasing diagrams technique is very useful for establishment of this property. Van Oostrom has further refined the technique by means of the decreasing proof order in his 2012 article. We have formalized the main two lemmas of this method, thereby verifying its correctness.