\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}