Christina Kohl, Aart Middeldorp
Proceedings of the 14th International Conference on Interactive Theorem Proving, Leibniz International Proceedings in Informatics 268, pp. 38:1-38:8, 2023.
pdf 
doi:10.4230/LIPIcs.ITP.2023.38
Abstract
We report on the first formalization of the almost-development closedness criterion for confluence of left-linear term rewrite systems and illustrate a problem we encountered while trying to formalize the original paper proof by van Oostrom.
BibTex
@inproceedings{CKAM-ITP23, author = "Christina Kohl and Aart Middeldorp", title = "Formalizing Almost Development Closed Critical Pairs", booktitle = "Proceedings of the 14th International Conference on Interactive Theorem Proving", editor = "Adam Naumowicz and Ren\'e Thiemann", series = "Leibniz International Proceedings in Informatics", volume = 268, pages = "38:1--38:8", year = 2023, doi = "10.4230/LIPIcs.ITP.2023.38"}