\begin{frame}[t]
  \frametitle{Transfinite Reductions}
  
  \vspace{-2ex}
  \begin{definition}
  Let $\alpha$ be an ordinal, 
  and $\tau : (t_\beta \to t_{\beta+1})_{\beta < \alpha}$ a sequence of reduction steps.
  \medskip\pause

  We use $d_\beta$ to denote the depth of the rewrite step $t_\beta \to t_{\beta+1}$.
  \bigskip\pause

  Then $\tau$ is an \alert{infinite reduction} of length $\alpha$ if for every limit ordinal $\lambda < \alpha$:
  \begin{enumerate}
    \item
    the distance $d(t_\beta,t_\lambda)$ tends to $0$,
    \hfill\textcolor{gray}{$\forall \epsilon > 0. \; \exists \beta < \lambda. \; \forall \beta < \gamma < \lambda.\; d(t_{\gamma},t_\lambda) \le \epsilon$} 
    \item 
    the depth $d_\beta$ tends to infinity
    \hfill\textcolor{gray}{$\forall n. \; \exists \beta < \lambda. \; \forall \beta < \gamma < \lambda.\; d_\gamma \ge n$} 
  \end{enumerate}
  as $\beta$ approaches $\lambda$ from below.
  \end{definition}
  \pause
  
  \alt<5>{
  \begin{example}[We want more than Cauchy-convergence\ldots]
  Let $R = \{f(x) \to f(c(x))\}$. Condition (2) excludes sequences like:
  $$f(a) \to_\epsilon f(c(a)) \to_\epsilon f(c(c(a))) \to_\epsilon \ldots \to^\omega_\epsilon f(c^\omega) \to \ldots $$
  where the \alert{activity does not move downwards}.
  \end{example}
  }{
  \begin{example}
  Let $R = \{a \to a,\; b\to b\}$. Condition (1) excludes \alert{jumps in the limit}:
  $$a\to a \to a \to \ldots \underbrace{b}_{t_\omega} \to b \to \ldots$$
  \end{example}
  }
\end{frame}