Abstract reduction system

Abstract reduction system: is a pair $$

A , →

</math>, where the reduction $$

→

</math> is a binary relation on the set $A$, i.e., $$

→ ⊆ A × A

</math>. Instead of $$

a , b ∈ →

</math> we write $$

a → b

</math>.

Baader, Franz, and Tobias Nipkow. Term rewriting and all that. Cambridge university press, 1998.