Level-Confluence of 3-CTRSs in Isabelle/HOL
arXiv:1602.07115
Abstract
We present an Isabelle/HOL formalization of an earlier result by Suzuki, Middeldorp, and Ida; namely that a certain class of conditional rewrite systems is level-confluent. Our formalization is basically along the lines of the original proof, from which we deviate mostly in the level of detail as well as concerning some basic definitions.
In Proceedings of the 4th International Workshop on Confluence (IWC 2015)