\begin{frame}
  \frametitle{Dependency Pairs}

  Let $t_0$ be a minimal and $t_0 \to_R t_1 \to_R t_2 \to_R \ldots$ an infinite rewrite sequence.
  \medskip

  We consider the first root rewrite step $t_i \to t_{i+1}$:

  \begin{center}
    \includegraphics[width=0.7\textwidth]{../graphics/pstricks/dp_2}
  \end{center}
  \vspace{-1em}
  \pause
  
  Then
  $$t_{0,\#} \to_R \ldots \to_R t_{i,\#} \stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)} s_\#$$
  \pause
  Repeating the construction with $s$ yields:
  $$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$$
  an infinite rewrite sequence containing infinitely many $\DP(R)$ steps.
\end{frame}