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