129/144
\begin{frame}
  \small
  
  \begin{block}{Properties of Term Rewriting Systems}
  We consider TRSs $\atrs = \TRS$ as 
  \begin{center}
    ARSs $\langle \TT(\FF,\VV),\: \to_\atrs \rangle$
  \end{center}
  TRSs inherit the properties: CR, WCR, SN, WN, NF, \UN, \UNrew, \dots
  \end{block}
  
  \onslide<2->
  \begin{example}
  \begin{itemize}
    \item<3->
      A term $t \in \TT(\FF,\VV)$ is called terminating if $t$ admits
      no infinite rewrite sequence $t = t_1 \to t_2 \to t_3 \to \ldots$
    \item<4->
      A TRS $\TRS$ is called terminating if all terms in $\TT(\FF,\VV)$ are.
    \item<5-> \ldots
  \end{itemize}
  \end{example}
\end{frame}