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