56/87
\begin{frame}
  \begin{definition}
  A reduction of length $\alpha$ is \alert{strongly convergent}
  if for every limit ordinal $\lambda \alert{\boldsymbol\le} \alpha$
  the depth $d_\beta$ tends to infinity as $\beta$ approaches $\lambda$ from below,
  and \alert{divergent}, otherwise.
  \end{definition}
  \pause
  
  \begin{example}
  \begin{enumerate}
    \item $R = \{\; a \to b,\; b \to a \;\}$
          $$a \to b \to a \to b \to \ldots$$
          \pause 
          \ldots is a divergent rewrite sequence of length $\omega$.
          \pause
    \item $R = \{\; f(x,x) \to f(a,b),\; a \to c(a),\; b \to c(b \; \}$
          $$f(a,b) \to^\omega f(c^\omega,b) \to^\omega f(c^\omega,c^\omega) \to f(a,b)$$
          \pause 
          \ldots is a strongly convergent rewrite sequence of length $\omega\cdot 2 + 1$.
  \end{enumerate}
  \end{example}
  \pause
  
  \begin{lemma}
  A reduction $\tau$ is strongly convergent\\
  \hfill $\Longleftrightarrow$
  for every $n \in \NN$ there are only finitely many steps at depth $n$ in $\tau$.
  \end{lemma}
\end{frame}