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