\begin{frame} \small \begin{definition} \smallskip A \alert{rewrite strategy} $\SS$ is mapping that assigns to every reducible term $t$ a nonempty set of finite nonempty rewrite sequences starting from $t$. \begin{itemize} \item<2-> $\SS$ is \alert{deterministic} if $|\SS(t)| = 1$ for every reducible term $t$ \item<3-> $\SS$ \alert{normalizes} term $t$ if there are no infinite $\SS$ rewrite sequences starting from $t$ \item<4-> $\SS$ is \alert{normalizing} if it normalizes every term that has a normal form \item<5-> $\SS$ is \alert{perpetual} if every maximal $\SS$ rewrite sequence starting from any non-terminating term is infinite \end{itemize} \end{definition} \begin{definition}<5-> A rewrite sequence is \alert{maximal} if it is infinite, or it ends in a normal form. \end{definition} \bigskip \begin{lemma}<6-> \smallskip For terminating TRSs every strategy is \alert<6>{normalizing} and \alert<6>{perpetual}. \end{lemma} \end{frame}