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