LIPIcs.ITP.2023.38.pdf
- Filesize: 0.69 MB
- 8 pages
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.
Feedback for Dagstuhl Publishing