\begin{frame} \frametitle{Dependency Pairs, Termination Proofs} \begin{definition} A well-founded weakly monotone $\Sigma$-algebra $(A,\lbrack \cdot \rbrack,{>},{\succeq})$ consists of: \begin{itemize} \item a $\Sigma$-algebra $(A,[\cdot])$ with relations $>$, $\succeq$ on $A$ \item $>$ is well-founded, \item $\SN({>}/{\succeq})$ (compatibility), \hfill(e.g. ${>} \cdot {\succeq} \subseteq {>}$ suffices) \item for all $f \in \Sigma$ the function $[f]$ is monotone w.r.t. \emph{$\succeq$} \end{itemize} \end{definition} \pause \begin{theorem} $\SN(\DP(R)_\text{top}/R)$ if there exists a weakly monotone $\Sigma$-algebra s.t. % \begin{itemize} \item ${\DP(R)} \subseteq {>}$ \hfill \textcolor{gray}{that is, $\interpret{\ell,\alpha} > \interpret{r,\alpha}$ \quad $\forall \alpha,\; \ell \to r \in \DP(R)$} \item ${R} \subseteq {\succeq}$ \hfill \textcolor{gray}{that is, $\interpret{\ell,\alpha} \succeq \interpret{r,\alpha}$ \quad $\forall \alpha,\; \ell \to r \in R$} \end{itemize} \end{theorem} \pause \smallskip Advantages: \alert{no monotonicity for $>$}, and \alert{$\succeq$ not well-founded}. \end{frame}