\begin{frame}
  \small
  
  \begin{definition}
  Let $\rho = t_0 \to t_1 \to \ldots$ be a finite or infinite rewrite sequence.
  \begin{itemize}
  \pause
    \item Consider a redex occurrence $s$ is some term $t_n$ of $\rho$.
          \smallskip\pause
          
          Then $s$ is \alert{secured} if eventually there are no residuals of $s$ left.
          \smallskip\pause
          
          That is, there exits $m > n$ such that $t_m$ contains no residuals of $s$.       
          \smallskip
  \pause
    \item The reduction $\rho$ is \alert{fair} if every redex occurring in $\rho$ is secured.
  \end{itemize}
  \end{definition}
  \medskip\pause
  
  \begin{definition}
  A strategy $\SS$ is \alert{fair} if every every maximal $\SS$
  rewrite sequence is fair.
  \end{definition}
\end{frame}