\begin{frame} \frametitle{Minimal Terms} \begin{block}{} We call a term is \emph{minimal} if all its strict subterms are terminating. \end{block} \pause \begin{theorem} Let $R$ be a non-terminating TRS.\\ Then there exists a minimal term which is non-terminating. \end{theorem} \pause \begin{proof} Since $R$ is non-terminating, there exists a non-terminating term $t$.\medskip\pause We prove: every non-terminating term $t$ contains a minimal subterm.\medskip\pause We use induction on the term structure of $t$: \begin{itemize} \pause \item Base case: all strict subterms of $t$ are terminating. \pause Then $t$ is minimal itself. \pause \item Induction step: $t$ has a strict subterm $t'$ which is not terminating.\\\pause\medskip Then by IH the term $t'$ contains a minimal, non-terminating subterm $t''$.\\\pause The term $t''$ is a minimal non-terminating subterm of $t$. \end{itemize} \vspace{-1em} \end{proof} \end{frame}