\begin{frame}
  \small

  \begin{definition}
  A reduction $\rho = t_0 \to t_1 \to \ldots$ is \alert{cofinal}
  if for every $t_0 \to^* s$ there exists $t_n$ in $\rho$ such that $s \to^* t_n$.
  \end{definition}
  \medskip\pause
  
  \begin{definition}
  A strategy $\SS$ is \alert{cofinal} if every every maximal $\SS$
  rewrite sequence is cofinal.
  \end{definition}
  \medskip\pause
  
  \begin{theorem}
  Cofinal strategies are normalizing.
  \end{theorem}
  \pause

  \begin{proof}
  Let $\SS$ be a cofinal strategy.  
  \pause
  Let $t_0$ be a term that has a normal form $u$ ($t_0 \to^* u$).
  \medskip\pause
  
  Consider a maximal $\SS$ rewrite sequence $\rho : t_0 \to t_1 \to \ldots$ starting from $t_0$.
  \medskip\pause

  By cofinality there must be $t_n$ in $\rho$ such that $u \to^* t_n$.
  \medskip\pause
  
  Hence $t_n = u$ since $u$ is a normal form.
  \end{proof}  
\end{frame}