On Formalizing Decreasing Proof Orders
Summary
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.