\begin{frame}
  \small
  
  \begin{definitions}
  A \alert<1>{reduction order} is well-founded order $>$ on terms which is
  \begin{itemize}
  \item
  \makebox[5cm][l]{closed under contexts}
  $s > t \quad\Longrightarrow\quad
  \makebox[5mm][r]{$C[s]$} > C[t]$
  \smallskip
  \item
  \makebox[5cm][l]{closed under substitutions}
  $s > t \quad\Longrightarrow\quad
  \makebox[5mm][r]{$s\sigma$} > t\sigma$
  \end{itemize}
  \smallskip
  \end{definitions}
  
  \bigskip
  
  \begin{notation}<2->
  \smallskip
  \alert<2>{$\RR \subseteq {>}$} \quad if\quad
  $\ell > r$ for all rules $\ell \to r$ in $\RR$
  \end{notation}
  
  \bigskip
  
  \begin{theorem}<3->
  \smallskip
  TRS $\RR$ is terminating
  \quad$\iff$\quad
  $\RR \subseteq {>}$ for reduction order $>$
  \end{theorem}
\end{frame}