\begin{frame}<2->
  \small
  
  \begin{example}[Combinatory Logic]
  \vspace{-2ex}
  \GREEN{\begin{xalignat*}{3}
  \m{I} \cdot x
  &\makebox[6mm][c]{$\alt<2->{\to}{\approx}$} x
  & \onslide<3->{\m{I}\,x} &\onslide<3->{\makebox[6mm][c]{$\to$} x}
  & \onslide<4->{\m{I}\,x} &\onslide<4->{\makebox[6mm][c]{$\to$} x}
  \\
  (\m{K} \cdot x) \cdot y
  &\makebox[6mm][c]{$\alt<2->{\to}{\approx}$} x
  & \onslide<3->{(\m{K}\,x)\,y} &\onslide<3->{\makebox[6mm][c]{$\to$} x}
  & \onslide<4->{\m{K}\,x\,y} &\onslide<4->{\makebox[6mm][c]{$\to$} x}
  \\
  ((\m{S} \cdot x) \cdot y) \cdot z
  &\makebox[6mm][c]{$\alt<2->{\to}{\approx}$} (x \cdot z) \cdot (y \cdot z)
  & \onslide<3->{((\m{S}\,x)\,y)\,z}
  &\onslide<3->{\makebox[6mm][c]{$\to$} (x\,z)\,(y\,z)}
  & \onslide<4->{\m{S}\,x\,y\,z}
  &\onslide<4->{\makebox[6mm][c]{$\to$} x\,z\,(y\,z)}
  \end{xalignat*}}
  \vspace{-3ex}
  \begin{itemize}
  \item<3->
  \alert<3,4>{applicative notation}: surpress $\cdot$
  \onslide<4->and adopt left-association
  \item<5->
  CL is confluent but not terminating
  \[
  \GREEN{
  \m{SII(SII)}
  \to \m{I(SII)(I(SII))}
  \to \m{SII(I(SII))}
  \to \m{SII(SII)}
  }
  \]
  \item<6->
  CL is \alert<6->{consistent}
  \[
  \GREEN{\m{S} \not\conv \m{K}}
  \]
  \vspace{-3ex}
  \end{itemize}
  \end{example}

\end{frame}