\begin{frame}
  \small
  
  \begin{theorem}
  \smallskip
  TRS $\RR$ is terminating ~$\iff$~
  $\RR \subseteq {>_\AA}$ for well-founded monotone algebra $(\AA,>)$
  \end{theorem}
  \pause
  \bigskip

  \begin{proof}
  \begin{itemize}
  \pause
    \item [$\Leftarrow$] Follows since we have shown that $>_\AA$ is a reduction order.
  \pause
    \item [$\Rightarrow$]
      As $\Sigma$-algebra we take $(A,[\cdot],{>})$ with 
      \begin{itemize}
      \pause
       \item $A = \TTlong$,
      \pause
       \item $\interpret{f}(t_1,\ldots,t_n) = f(t_1,\ldots,t_n)$,
      \pause
       \item ${>} := {\to}$.
      \end{itemize}
      \pause\smallskip
      Then $>$ is well-founded since $R$ is terminating.\\
      \pause\smallskip
      Monotonicity of $>$ follows from closure of $\to$ under contexts:\\[-2em]
      $$
      s > t \Rightarrow [f](\ldots,s,\ldots) = f(\ldots,s,\ldots) > f(\ldots,t,\ldots) = [f](\ldots,t,\ldots)
      $$
      \vspace{-1.5em}
      
      \pause
      ${R} \subseteq {>_\AA}$ since for all $\ell \to r \in R$ and $\alpha : {\cal X} \to A$:\\[-1em]
      $$\interpret{\ell,\alpha} = \ell\alpha > r\alpha = \interpret{r,\alpha}.$$
      \vspace{-2.5em}
  \end{itemize}
  \end{proof}
\end{frame}