Reductions in Higher-Order Rewriting and Their Equivalence

Pablo Barenbaum, Eduardo Bonelli

Proof terms are syntactic expressions that represent computations in term rewriting. They were introduced by Meseguer and exploited by van Oostrom and de Vrijer to study equivalenc…