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