Term rewriting for equational theories

Definition

Let $\sigma$ be a signature and $X$ a set of variables. Let $T(X)$ be the set of terms of $\sigma$ over $X$, as in the term algebra. A term rewriting system is a set $R$ of pairs $(l, r)$ of terms, written $l \to r$ and called rules. Each rule must satisfy two conditions: $l$ is not a variable, and every variable of $r$ occurs in $l$. For terms $s, t$, one writes $s \to_R t$ if there are a rule $l \to r$ in $R$ and a substitution $\tau$ with the following property. The term $s$ contains $\tau(l)$ as a subterm, and $t$ is obtained from $s$ by replacing one occurrence of it by $\tau(r)$. Let $\leftrightarrow_R^*$ be the smallest equivalence relation that contains $\to_R$. The system $R$ presents the equational theory $E$ if, for all terms $s, t$, one has $s \leftrightarrow_R^* t$ if and only if $s \approx t$ belongs to $E$. The system $R$ is convergent if:

1. it is terminating: there is no infinite chain $t_0 \to_R t_1 \to_R t_2 \to_R \cdots$;
2. it is confluent: if $t \to_R^* u$ and $t \to_R^* v$, then $u \to_R^* w$ and $v \to_R^* w$ for some term $w$.