\begin{frame}[t]
  \frametitle{Dependency Pairs, Introduction}
  
  \alert<1>{Assume $R$ is non-terminating.} \pause
  There exists a minimal, non-terminating term $t_0$.
  $$t_0 \to_R t_1 \to_R t_2 \to_R \ldots$$
  \pause
  \vspace{-1.5em}
  
  \begin{block}{}
  At some point there must be a root step $t_i \to t_{i+1}$.
  \end{block}
  \pause
  
  \begin{proof}
  Assume all steps would be below the root. Then:
  \begin{itemize}
    \item all $t_i$ are minimal,
    \item all rewrite steps are in terminating terminating.
  \end{itemize}
  \end{proof}
  \pause
  \bigskip
  
  Notation: we use $\stackrel{\text{\tiny top}}{\longrightarrow}_R$
  to denote root rewrite steps.
\end{frame}