236/365
\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}