\begin{frame}
  \small
  
  \begin{example}[Group Theory]
  \smallskip
  \begin{tabular}{l@{\qquad}lc}
  signature &
  $\mG{e}$ ~ (constant) \quad \GREEN{${}^-$} ~ (unary, postfix)
  \quad \GREEN{$\cdot$} ~ (binary, infix) \\
  \\[-1ex]
  ES &
  \GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l@{\qquad}r@{~}c@{~}l@{\qquad}%
  r@{~}c@{~}l@{}}
  \m{e} \cdot x &\approx& x &
  x^- \cdot x &\approx& \m{e} &
  (x \cdot y) \cdot z &\approx& x \cdot (y \cdot z)
  \end{array}$} & $\EE$ \\
  \\[-1ex]
  theorems &
  $\begin{array}[t]{@{\qquad\qquad}r@{~}c@{~}l@{\qquad}%
  r@{~}c@{~}l@{}}
  \m{e}^-
  &\makebox[5mm]{$\!\alert<3>{\alt<3->{\downarrow_\RR}{\approx_\EE}}$}&
  \m{e} &
  (x \cdot y)^-
  &\makebox[5mm]{$\!\alert<3>{\alt<3->{\downarrow_\RR}{\approx_\EE}}$}&
  y^- \cdot z^-
  \end{array}$ \\
  \\[-1ex]
  TRS &
  \GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l@{\quad}r@{~}c@{~}l@{}}
  \m{e} \cdot x &\to& x &
  x \cdot \m{e} &\to& x
  \\
  x^- \cdot x &\to& \m{e} &
  x \cdot x^- &\to& \m{e}
  \\
  (x \cdot y) \cdot z &\to& x \cdot (y \cdot z) &
  x^{- -} &\to& x
  \\
  \m{e}^- &\to& \m{e}
  & (x \cdot y)^- &\to& y^- \cdot x^-
  \\
  x^- \cdot (x \cdot y) &\to& y &
  x \cdot (x^- \cdot y) &\to& y
  \end{array}$} & $\RR$
  \end{tabular}
  
  \smallskip
  
  \begin{itemize}
  \item<2->
  $\RR$ is complete and 
  $\xleftrightarrow[\EE]{*} ~=~ \xleftrightarrow[\RR]{*}$
  \quad$\Longrightarrow$\quad
  $\EE$ has decidable validity problem
  \item<4->
  \makebox[8.6cm][l]{How to compute $\RR$ ?}
  \onslide<5->{\alert{completion}}
%   (lectures 5 \& 6)}
%   \item<6->
%   \makebox[5cm][l]{how to prove termination of $\RR$ ?}
%   \onslide<7->{\makebox[25mm][l]{\alert{LPO} or \alert{KBO}}
%   (lectures 4 \& 7)}
  \smallskip
  \end{itemize}
  \end{example}
\end{frame}