\begin{frame}
  \frametitle{Dependency Pairs, Main Theorem}
  
  \begin{definition}[Relative Termination]
    A relation $\to_1$ is called \alert{terminating  relative to $\to_2$}, denoted \alert{$\SN(\to_1/\to_2)$},\\ if
    every ${\to_1} \cup {\to_2}$ rewrite sequence contains only finitely many $\to_1$ steps.
  \end{definition}
  \pause
  
  \begin{lemma}
   $$\SN(\to_1/\to_2) \quad\Longleftrightarrow\quad \SN(\to_2^* \cdot \to_1 \cdot \to_2^*)$$
  \end{lemma}
  \pause
  \bigskip
  
  The main theorem from dependency pairs is:
  \begin{theorem}
  \centerline{$\SN(R) \quad\Longleftrightarrow\quad \SN(\DP(R)_\text{top}/R)$}
  \end{theorem}
  \pause
  
  That is, a TRS $R$ is terminating if and only if 
  $\stackrel{\text{\tiny top}}{\longrightarrow}_{\DP(R)}$
  terminates relative to
  $\to_R$.
\end{frame}