\begin{frame} \small \begin{definition} \smallskip An \alert<1>{equational system} (\alert<1>{ES}) is pair $\ES$ consisting of \begin{itemize} \item \makebox[1cm][l]{$\FF$} signature \item \makebox[1cm][l]{$\EE$} set of equations between terms in $\TT(\FF,\VV)$ \end{itemize} \end{definition} \bigskip \begin{example}<2-> \smallskip ES $(\FF,\EE)$ with signature $\FF$ \[ \mG{0} ~ (\text{constant}) \qquad \mG{s} ~ (\text{unary}) \qquad \GREEN{+} ~ (\text{binary, infix}) \] and equations $\EE$ \[ \GREEN{\begin{array}{r@{~}c@{~}l} \m{0}+y & \approx & y \\[.5ex] \m{s}(x)+y & \approx & \m{s}(x+y) \end{array}} \] \end{example} \end{frame}