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