30/251
\begin{frame}
\small

\begin{example}[Group Theory]
\smallskip
$\mG{e}$ ~ (constant) \quad \GREEN{${}^-$} ~ (unary, postfix)
\quad \GREEN{$\cdot$} ~ (binary, infix) \\
\\[-1ex]
\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]
\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 z^- \end{array}$} \\
\\[-1ex]
\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}