\begin{frame}
  \small
  
  \vspace{-1ex}
  
  \begin{lemma}
  \smallskip
  TRS $\RR$ is terminating \\
  \qquad $\iff$ \\
  $\exists$ well-founded order $>$ on terms such that
  $s > t$ whenever \alert<4>{$s \to_\RR t$}
  \end{lemma}
  
  \begin{example}<2->
  \smallskip
  \begin{itemize}
  \item
  TRS
  \vspace{-2ex}
  \GREEN{\begin{xalignat*}{2}
  \m{0}+y &\to y & \m{s}(x)+y &\to \m{s}(x+y)
  \end{xalignat*}}
  \vspace{-4ex}
  \item<3->
  well-founded order $>$
  \vspace{-3ex}
  \[
  s > t \quad\iff\quad \varphi(s) >_\NN \varphi(t)
  ~ \text{with $\varphi(u) = \begin{cases}
  1 & \text{if $u = \mG{0}$} \\
  \varphi(v)+1 & \text{if $u = \mG{s}(v)$} \\
  2\varphi(v)+\varphi(w) & \text{if $u = \GREEN{\BLACK{v}+\BLACK{w}}$} \\
  0 & \text{otherwise}
  \end{cases}$}
  \]
  \vspace{-3ex}
  \end{itemize}
  \end{example}
  
  \begin{remark}<4->
  \smallskip
  (very) inconvenient to check all rewrite \alert{steps}
  \end{remark}
  
\end{frame}