\begin{frame}
  \frametitle{Infinitary Rewriting}
  
  \begin{example}
  \vspace{-2ex}
  \begin{align*}
    f(x,x) &\to f(a,b)\\
    a &\to c(a)\\
    b &\to c(b)
  \end{align*}
  \end{example}

  \pause\vspace{-2ex}
  \begin{align*}
    f(a,b) 
    &\pause\to f(c(a),b)\\
    &\pause\to f(c(c(a)),b)\\
    &\pause\ired f(c(c(c(\ldots))),b)\\
    &\pause\to f(c(c(c(\ldots))),c(b))\\
    &\pause\to f(c(c(c(\ldots))),c(c(b)))\\
    &\pause\ired f(c(c(c(\ldots))),c(c(c(\ldots))))\\
    &\pause\to f(a,b)\\
    &\pause\to \ldots
  \end{align*}
  \pause\vspace{-3ex}
  
  We need transfinite reductions\ldots
  \bigskip 
\end{frame}