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.

BibTeX

@inproceedings{CSTS-IWC15,
 author    = "Christian Sternagel and Thomas Sternagel",
 title     = "Level-Confluence of 3-{CTRSs} in {Isabelle/HOL}",
 booktitle = "Proceedings of the 4th International Workshop on Confluence",
 pages     = "28--32",
 year      = 2015
}