\begin{frame}
  \begin{block}{Comparison finitary vs. infinitary rewriting}  
  \renewcommand{\arraystretch}{1.2}
  \begin{center}
    \begin{tabular}{|c|c|}
    \hline
    \textbf{finitary rewriting} & \textbf{infinitary rewriting} \\
    \hline
    finite reduction & strongly convergent reduction\\
    \hline
    infinite reduction & divergent reduction\\
    \hline
    \end{tabular}
  \end{center}
  \end{block}
  \pause
  
  \begin{definition}
  Let $\atrs$ be a TRS and $s$ a term. Then the term $s$ is
  \begin{itemize}
    \item 
      \alert{infinitary strongly normalizing} (\alert{$\SNi$})
      if $s$ admits no divergent reductions,
    \item 
      \alert{infinitary weakly normalizing} (\alert{$\WNi$})
      if $s$ admits a reduction to normal form,
    \item 
      \alert{infinitary confluent} (\alert{$\CRi$})
      if $\forall t_1 \iredi s \ired t_2.\; t_1 \ired \cdot \iredi t_2$.
  \end{itemize} 
  Likewise $\atrs$ has the respective property if all terms from $\iter$ have.
  \end{definition}
  \pause
  
  \begin{example}
  \begin{itemize}
    \item Let $R = \{\;a \to c(a)\;\}$. \pause Then $R$ is $\WNi$, $\SNi$ and $\CRi$. 
  \pause
    \item Let $R = \{\;a \to a,\; a \to c(a)\;\}$. \pause Then $R$ is $\WNi$ and $\CRi$, but not $\SNi$. 
  \end{itemize}
  \end{example}
\end{frame}