\begin{frame}
  \begin{theorem}
  \smallskip
  TRS $\RR$ is terminating
  \quad$\iff$\quad
  $\RR \subseteq {>}$ for reduction order $>$
  \end{theorem}

  \begin{proof}[Proof $\Leftarrow$]
  \pause
  Let $>$ be reduction order such that ${R} \subseteq {>}$.\pause\medskip

  Recall that $\to$ is the smallest relation $S$ such that:
  \begin{itemize}
    \item ${R} \subseteq {S}$,
    \item $S$ is closed under contexts, and
    \item $S$ is closed under substitutions.
  \end{itemize}
  \pause
  
  Then ${\to} \subseteq {>}$ since ${>}$ has these properties.
  \medskip
  \pause
  
  Assume there exists an infinite rewrite sequence:
  $t_0 \to t_1 \to t_2 \ldots$
  \medskip
  \pause
  
  Then also
  $t_0 > t_1 > t_2 \ldots$ since ${\to} \subseteq {>}$
  \medskip
  \pause  
  
  However, this contradicts well-foundedness of $>$.
  \end{proof}
\end{frame}