\begin{frame}
  Steps below the root do not change minimality:
  
  \pause
  \begin{lemma}
    Let $t$ be minimal and $t \to s$ a rewrite step below the root.
    Then $s$ is minimal.
  \end{lemma}
  \pause
  
  \begin{proof}
    We have $t = f(t_1,\ldots,t_n)$ and $s = f(s_1,\ldots,s_n)$ and $i \in \nat$ such that:
    \begin{itemize}
      \item $t_i \to s_i$, and
      \item $t_j = s_j$ for all $j \ne i$.
    \end{itemize}
    \pause\medskip
  
    Then since $t$ is minimal, it follows that all $t_k$ are terminating.
    \pause\medskip
    
    Since $t_k \to^* s_k$, we obtain $s_k$ is terminating for all $1 \le k \le n$.
    \pause\medskip
    
    Hence $s$ is minimal.
  \end{proof}
\end{frame}