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