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


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.

Nach oben scrollen