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