A Formalization of Newman's and Yokouchi's Lemmas in a Higher-Order Language

Andre Luiz Galdino & Mauricio Ayala-Rincón
This paper shows how a formalization for the theory of Abstract Reduction Systems (ARSs) in which noetherianity was specified by the notion of well-foundness over binary relations is used in order to prove results such as the well-known Newman's and Yokouchi's Lemmas. The former is known as the diamond lemma and the latter states a property of commutation between ARSs. The theory ars was specified in the Prototype Verification System (PVS) for which to the...