\begin{frame} \small \begin{definitions}[Properties of Elements] Let $\langle A, \to \rangle$ be an ARS. An element $a\in A$ is called: \begin{itemize} \item<2-> \makebox[1.5cm][l]{\alert<2>{SN}} \alert<2>{strongly normalizing} \quad or\quad \alert<2>{terminating}\\[1ex] if $a$ admits no infinite rewrite sequence $a = a_1 \to a_2 \to \ldots$ \smallskip \item<3-> \makebox[1.5cm][l]{\alert<3>{WN}}\alert<3>{weakly normalizing}\\[1ex] if $\exists b.\; a \to^! b$ \smallskip \item<4-> \makebox[1.5cm][l]{\alert<4>{CR}} \alert<4>{confluent} \quad or\quad \alert<4>{Church Rosser}\\[1ex] if $\forall b,c.\; (c \FromP{*} a \to^* b \;\Rightarrow\; \exists d.\; c \to^* d \FromP{*} b)$ \smallskip \item<5-> \makebox[1.5cm][l]{\alert<5>{WCR}} \alert<4>{weakly confluent} \quad or\quad \alert<5>{weakly Church Rosser}\\[1ex] if $\forall b,c.\; (c \from a \to b \;\Rightarrow\; \exists d.\; c \to^* d \FromP{*} b)$ \smallskip \end{itemize} \end{definitions} \onslide<6-> \begin{block}{} An ARS has the property if all its elements have the respective property. \end{block} \end{frame}