\begin{frame}
\small

\begin{examples}
\smallskip
\begin{itemize}
\item
$\GREEN{x+\m{s}(y+z)}$ matches $\GREEN{\m{s}(y)+\m{s}((x+\ms{s}(0))+z)}$%
\onslide<2->:
\begin{align*}
& \hspace{-2cm}
\{ \GREEN{x \alert<3>{+} \m{s}(y+z)} \mapsto
\GREEN{\m{s}(y) \alert<3>{+} \m{s}((x+\ms{s}(0))+z)} \}
\\
\onslide<3->{\Longrightarrow} \quad &
\makebox[6cm][l]{$\onslide<3->{\{ \GREEN{x} \mapsto \GREEN{\m{s}(y)},\:
\GREEN{\alert<4>{\m{s}}(y+z)} \mapsto
\GREEN{\alert<4>{\m{s}}((x+\ms{s}(0))+z)} \}}$}
\\
\onslide<4->{\Longrightarrow} \quad &
\onslide<4->{\{ \GREEN{x} \mapsto \GREEN{\m{s}(y)},\:
\GREEN{y \alert<5>{+} z} \mapsto \GREEN{(x \alert<5>{+} \ms{s}(0))+z} \}}
\\
\onslide<5->{\Longrightarrow} \quad &
\onslide<5->{\{ \GREEN{x} \mapsto \GREEN{\m{s}(y)},\:
\GREEN{y} \mapsto \GREEN{x+\ms{s}(0)},\:
\GREEN{z} \mapsto \GREEN{z} \}}
\end{align*}
\item<6->
$\GREEN{x^{-} \cdot (x \cdot y)}$ does not match
$\GREEN{(\m{e} \cdot x)^{-} \cdot ((\m{e} \cdot \m{e}) \cdot x)}$:
\begin{align*}
& \hspace{-2cm}
\{
\GREEN{x^{-} \alert<7>{\cdot} (x \cdot y)} \mapsto
\GREEN{(\m{e} \cdot x)^{-} \alert<7>{\cdot} ((\m{e} \cdot \m{e}) \cdot x)}
\}
\\
\onslide<7->{\Longrightarrow} \quad &
\makebox[6cm][l]{$\onslide<7->{\{ \GREEN{x^{\alert<8>{-}}} \mapsto
\GREEN{(\m{e} \cdot x)^{\alert<8>{-}}},\:
\GREEN{x \cdot y} \mapsto \GREEN{(\m{e} \cdot \m{e}) \cdot x} \}}$}
\\
\onslide<8->{\Longrightarrow} \quad &
\onslide<8->{\{ \GREEN{x} \mapsto \GREEN{\m{e} \cdot x},\:
\GREEN{x \alert<9>{\cdot} y} \mapsto
\GREEN{(\m{e} \cdot \m{e}) \alert<9>{\cdot} x} \}}
\\
\onslide<9->{\Longrightarrow} \quad &
\onslide<9->{\{ \GREEN{x} \mapsto \GREEN{\alert<10>{\m{e} \cdot x}},\:
\GREEN{x} \mapsto \GREEN{\alert<10>{\m{e} \cdot \m{e}}},\:
\GREEN{y} \mapsto \GREEN{x} \}}
\\
\onslide<10->{\Longrightarrow} \quad &
\onslide<10->{\bot}
\end{align*}
\vspace{-3ex}
\end{itemize}
\end{examples}

\end{frame}