\begin{frame} \small \begin{definition} \smallskip For every ES $\ES$ we define TRS $\atrs_\EE = (\Sigma,R)$ with rules: \[ R = \{\ell \to r \mid \ell \approx r \in \EE \text{ or } r \approx \ell \in \EE\} \]\vspace{-3ex} For $\leftrightarrow_{\atrs_\EE}$ we write $\leftrightarrow_\EE$ for short. \end{definition} \smallskip\pause \begin{example} \smallskip ES $\EE = \{ \GREEN{\m{0}+y \approx y},~\GREEN{\m{s}(x)+y \approx \m{s}(x+y) } \}$ \begin{align*} R = \{\ &\m{0}+y \to y,\\ &y \to \m{0}+y,\\ &\m{s}(x)+y \to \m{s}(x+y),\\ &\m{s}(x+y) \to \m{s}(x)+y\ \} \end{align*} \end{example} \smallskip\pause \begin{theorem} \smallskip $\forall$ ES $\EE$ \quad $\EE \vdash s \approx t \quad \Longleftrightarrow \quad s \leftrightarrow^*_\EE t$ %${\conv_\EE} ~=~ {\approx_\EE} ~=~ {=_\EE}$ \end{theorem} \end{frame}