\begin{frame}
\small

\begin{example}[Group Theory]
\smallskip
\begin{tabular}{l@{\qquad}lc}
\alert<1>{signature} &
$\mG{e}$ ~ (constant) \quad \GREEN{${}^-$} ~ (unary, postfix)
\quad \GREEN{$\cdot$} ~ (binary, infix) \\
\\[-1ex]
\onslide<2->\alert<2>{equations} &
\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]
\onslide<3->\alert<3>{theorems} &
\alert<3>{$\begin{array}[t]{@{\qquad\qquad}r@{~}c@{~}l@{\qquad}%
r@{~}c@{~}l@{}}
\m{e}^- &\approx_\EE& \m{e} &
(x \cdot y)^- &\approx_\EE& y^- \cdot x^-
\end{array}$} \\
\\[-1ex]
\onslide<4->\alert<4,5>{rewrite rules} &
\GREEN{$\begin{array}[t]{@{}r@{~}c@{~}l@{\quad}r@{~}c@{~}l@{}}
\m{e} \cdot x &\to& x &
\onslide<5->{x \cdot \m{e}} &\onslide<5->{\to}& \onslide<5->{x}
\\
x^- \cdot x &\to& \m{e} &
\onslide<5->{x \cdot x^-} &\onslide<5->{\to}& \onslide<5->{\m{e}}
\\
(x \cdot y) \cdot z &\to& x \cdot (y \cdot z) &
\onslide<5->{x^{- -}} &\onslide<5->{\to}& \onslide<5->{x}
\\
\onslide<5->{\m{e}^-} &\onslide<5->{\to}& \onslide<5->{\m{e}}
& \onslide<5->{(x \cdot y)^-} &\onslide<5->{\to}&
\onslide<5->{y^- \cdot x^-}
\\
\onslide<5->{x^- \cdot (x \cdot y)} &\onslide<5->{\to}& \onslide<5->{y} &
\onslide<5->{x \cdot (x^- \cdot y)} &\onslide<5->{\to}& \onslide<5->{y}
\end{array}$} & $\RR$
\end{tabular}

\smallskip

\begin{itemize}
\item<6->[\structure{\ding{192}}]~
$s \approx t$ is valid in $\EE$
($s \approx_\EE t$) if and only if $s$ and $t$ have same $\RR$-normal form
\item<7->[\structure{\ding{193}}]~
$\RR$ admits no infinite computations
\item<8->[\structure{\ding{192}}] \& \,\structure{\ding{193}}
\quad$\Longrightarrow$\quad
$\EE$ has decidable validity problem
\smallskip
\end{itemize}
\end{example}

\end{frame}