\begin{frame}
  \frametitle{Stepwise Termination Proofs}
  
  Stepwise termination proofs with dependency pairs:
  
  \begin{theorem}
  If there exists a weakly monotone $\Sigma$-algebra s.t.
  %
  \begin{itemize}
  \item ${T_1} \subseteq {>}$
  \item ${T_2 \cup R} \subseteq {\succeq}$
  \end{itemize}
  Then
  \vspace{-1.5ex}
  \begin{align*}
    \SN(T_{2,\text{top}}/R) \implies \SN((T_1 \cup T_2)_\text{top}/R)
  \end{align*}
  \end{theorem}
  \smallskip
  That is, we may remove the strictly decreasing \alert{top-rules}.
  \medskip\pause

  Typically, $T_1, T_2 \subseteq \DP(R)$.
  Works also for other top-termination problems.
  
  \medskip\pause
  We are \alert{not} allowed to remove strictly decreasing rules in $R$!\\
  For removing from $R$ we need monotonic interpretations!
\end{frame}