\begin{frame}
  \frametitle{Dependency Pairs}

  \begin{lemma}
  Let $R$ be a non-terminating TRS. Then there exists a rewrite sequence:
  $$t_{0,\#} \to_R^* \cdot \stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)} \cdot \to_R^* \cdot \stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)} \cdot \to_R^* \cdot \stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)} \ldots$$
  such that:
  \begin{itemize}
    \item the sequence contains infinitely many $\DP(R)$ steps,
    \item all $R$ steps are below the root, and
    \item all $\DP(R)$ steps are at the root.
  \end{itemize} 
  \end{lemma}
\end{frame}