\begin{frame}
  \begin{theorem}
  \smallskip
  TRS $\RR$ is terminating
  \quad$\iff$\quad
  $\RR \subseteq {>}$ for reduction order $>$
  \end{theorem}
  \begin{proof}[Proof $\Rightarrow$]
  \pause
  Let $R$ be terminating.\\[1em]
  \pause
  We define ${>} = {\to}$.\\[1em]
  \pause
  Then:
  \begin{itemize}
    \item $>$ is well-founded since $R$ is terminating,
  \pause
    \item $>$ is closed under substitutions since $\to$ is, and
  \pause
    \item $>$ is closed under contexts since $\to$ is.
  \end{itemize}
  \pause
  Hence $>$ is a reduction order. \pause Moreover ${R} \subseteq {\to}$.
  \end{proof}
\end{frame}