\begin{frame}
  \small

  \vspace{-1ex}
  
  \begin{theorem}
  \smallskip
  For orthogonal TRSs
  \begin{itemize}
  \item
  \structure{full substitution} and \structure{parallel outermost}
  strategies are \alert{normalizing}
  \vspace{-.5ex}
  \item<2->
  \structure{innermost} strategies are \alert{perpetual}
  \vspace{-.5ex}
  \item<3->
  \structure{leftmost outermost} strategy is \alert{not normalizing}
  \vspace{-.5ex}
  \item<4->
  \structure{full substitution} is \alert{fair}
  \end{itemize}
  \smallskip
  \end{theorem}
  
  \begin{example}<4->
  \vspace{-2ex}
  \GREEN{\begin{xalignat*}{3}
  \m{a} &\to \m{b} & \m{c} &\to \m{c} & \m{f}(x,\m{b}) &\to \m{b}
  \end{xalignat*}}
  \vspace{-4.5ex}
  \begin{itemize}
  \item
  \makebox[35mm][l]{\structure{leftmost outermost}}
  \GREEN{\(
  \m{f}(\alert<5->{\m{c}},\m{a})
  \onslide<5->{\to \m{f}(\alert<6->{\m{c}},\m{a})}
  \onslide<6->{\to \m{f}(\alert<7->{\m{c}},\m{a})}
  \onslide<7->{\to \cdots}
  \)}
  \item
  \makebox[35mm][l]{\structure{leftmost innermost}}
  \GREEN{\(
  \m{f}(\alert<8->{\m{c}},\m{a})
  \onslide<8->{\to \m{f}(\alert<9->{\m{c}},\m{a})}
  \onslide<9->{\to \m{f}(\alert<10->{\m{c}},\m{a})}
  \onslide<10->{\to \cdots}
  \)}
  \item
  \makebox[35mm][l]{\structure{parallel outermost}}
  \GREEN{\(
  \m{f}(\alert<11->{\m{c}},\alert<11->{\m{a}})
  \onslide<11->{\parr \alert<12->{\m{f}}(\m{c},\m{b})}
  \onslide<12->{\to \m{b}}
  \)}
  \item
  \makebox[35mm][l]{\structure{parallel innermost}}
  \GREEN{\(
  \m{f}(\alert<13>{\m{c}},\alert<13->{\m{a}})
  \onslide<13->{\parr \m{f}(\alert<14->{\m{c}},\m{b})}
  \onslide<14->{\to \m{f}(\alert<15->{\m{c}},\m{b})}
  \onslide<15->{\to \cdots}
  \)}
  \item
  \makebox[35mm][l]{\structure{full substitution}}
  \GREEN{\(
  \m{f}(\alert<16->{\m{c}},\alert<16->{\m{a}})
  \onslide<16->{\dev \alert<17->{\m{f}}(\alert<17->{\m{c}},\m{b})}
  \onslide<17->{\dev \m{b}}
  \)}
  \end{itemize}
  \end{example}
\end{frame}