\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}