Lifting Term Rewriting Derivations in Constructor Systems by Using Generators

Adrián Riesco, Juan Rodríguez-Hortalá

Narrowing is a procedure that was first studied in the context of equational E-unification and that has been used in a wide range of applications. The classic completeness result d…