\begin{frame}[t]
  \frametitle{Subterm Criterion}
  
  \begin{theorem}[Subterm Criterion]
    Let $R$ be a TRS, $T_1,T_2 \subseteq \DP(R)$, and $\pi : \Sigma_\# \to \nat$ such that:
    \begin{itemize}
      \item $s_{\pi(f_\#)} \triangleright t_{\pi(g_\#)}$ for every rule
            $f_\#(s_1,\dots,s_n) \to g_\#(t_1,\ldots,t_m) \in T_1$ 
      \item $s_{\pi(f_\#)} = t_{\pi(g_\#)}$ for every rule
            $f_\#(s_1,\dots,s_n) \to g_\#(t_1,\ldots,t_m) \in T_2$ 
    \end{itemize}
    Then:
    \vspace{-1em}
    \begin{align*}
      \SN(T_{2,\mit{top}}/R) \implies \SN((T_1 \cup T_2)_{\mit{top}}/R)
    \end{align*}
  \end{theorem}
  \pause
  \medskip
  
  \begin{proof}
  After the dependency pairs transformation, we consider only \emph{minimal terms}.
  \pause
  \medskip
  
  We can only finitely often make a terminating term smaller ($\triangleright$).
  \end{proof}
\end{frame}