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