\begin{frame}
  \small
  
  \begin{definition}
  \smallskip
  A TRS is \alert{left-normal} if variables do not precede function symbols
  in left-hand sides (where the left-hand sides are written in prefix notation).
  \end{definition}
  
  \smallskip
  
  \begin{example}<2->
  \begin{itemize}
  \item
  \makebox[4cm][l]{$\GREEN{\m{f}(\alert<3->{x},\; \m{g}(y,z)) \to
  \m{g}(y,\; \m{f}(x,z))}$}
  \qquad
  \onslide<3->{$\huil$}
  \item<4->
  \makebox[4cm][l]{$\GREEN{\m{f}(\m{g}(x,y),\; z) \to \m{g}(x,\; \m{g}(y,z))}$}
  \qquad
  \onslide<5->{$\lach$}
  \smallskip
  \end{itemize}
  \end{example}
  
  \smallskip
  
  \begin{theorem}<6->
  \smallskip
  \structure{Leftmost outermost} strategy is normalizing for
  orthogonal left-normal TRSs.
  \end{theorem}
  
  \smallskip
  
  \begin{block}<7->{Remark}
  \smallskip
  %easy but \alert<7>{important} result:
  \alert{Combinatory Logic} is left-normal
  \GREEN{\begin{xalignat*}{3}
  \m{I}\,x &\to x &
  \m{K}\,x\,y &\to x &
  \m{S}\,x\,y\,z &\to x\,z\,(y\,z)
  \end{xalignat*}}
  \vspace{-4ex}
  \end{block}
\end{frame}