\begin{frame}
  \small
  
  \vspace{-1ex}
  
  \begin{definition}
  \smallskip
  For orthogonal TRSs the \alert{full substitution} strategy performs
  \alert{complete development} of all redexes.
  \smallskip
  \end{definition}
  
  \smallskip
  
  \begin{example}<2->
  \smallskip
  \begin{itemize}
  \item
  rewrite rules
  \vspace{-1ex}
  \GREEN{\begin{xalignat*}{2}
  \m{0} + y & \to y &
  \m{0} \times y &\to \m{0} \\
  \m{s}(x) + y &\to \m{s}(x + y) &
  \m{s}(x) \times y &\to (x \times y) + y 
  \end{xalignat*}}
  \vspace{-5ex}
  \item
  full substitution strategy
  \GREEN{\begin{align*}
  \m{s}(\m{s}(\m{0}))& {} \alert{\times}
  (\m{s}(\m{0}) \alert{+} \m{s}(\m{s}(\m{0}))) \\
  &\onslide<3->{\dev 
  (\m{s}(\m{0}) \alert{\times} \m{s}(\m{0} \alert{+} \m{s}(\m{s}(\m{0})))) +
  \m{s}(\m{0} \alert{+} \m{s}(\m{s}(\m{0})))}
  \\
  &\onslide<4->{\dev 
  ((\m{0} \alert{\times} \m{s}(\m{s}(\m{s}(\m{0})))) + \m{s}(\m{s}(\m{s}(\m{0})))) +
  \m{s}(\m{s}(\m{s}(\m{0})))}
  \\
  &\onslide<5->{\to 
  (\m{0} \alert{+} \m{s}(\m{s}(\m{s}(\m{0})))) + \m{s}(\m{s}(\m{s}(\m{0})))}
  \\
  &\onslide<6->{\to 
  \m{s}(\m{s}(\m{s}(\m{0}))) \alert{+} \m{s}(\m{s}(\m{s}(\m{0})))} \\
  &\onslide<7->{\to \ldots \to 
  \m{s}(\m{s}(\m{s}(\m{s}(\m{s}(\m{s}(\m{0}))))))}
  \end{align*}}
  \vspace{-4ex}
  \end{itemize}
  \end{example}
\end{frame}