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