### Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting

Alexander Lochmann, Aart Middeldorp26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, LCNS 12079, pp. 25 – 40, 2020.

### Abstract

We present a formalized proof of the regularity of the infinity predicate on ground terms. This predicate plays an important role in the first-order theory of rewriting because it allows to express the termination property. The paper also contains a formalized proof of a direct tree automaton construction of the normal form predicate, due to Comon.

### BibTeX

@inproceedings{LM-TACAS20, author = "Alexander Lochmann and Aart Middeldorp", title = "Formalized Proofs of the Infinity and Normal Form Predicates in the First-Order Theory of Rewriting", booktitle = "Proceedings of the 26th International Conference on Tools and Algorithms for the Construction and Analysis of Systems", editor = "Armin Biere and Dave Parker", series = "Lecture Notes in Computer Science", volume = 12079, pages = "178--194", year = 2020, doi = "10.1007/978-3-030-45237-7_11" }

The Author(s) 2020