Reducing Rewrite Properties to Properties on Ground Terms

Alexander Lochmann

2 June 2022


This AFP entry relates important rewriting properties between the set of terms and the set of ground terms induced by a given signature. The properties considered are confluence, strong/local confluence, the normal form property, unique normal forms with respect to reduction and conversion, commutation, conversion equivalence, and normalization equivalence.
BSD License

Depends On