\begin{frame} \small \begin{definitions} \begin{itemize} \item term $t$ is \alert<1>{linear} is each variable in $\Var(t)$ occurs exactly once in $t$ \item<2-> rewrite rule $\ell \to r$ is \alert<2>{left-linear} if $\ell$ is linear \item<3-> TRS is left-linear if all rewrite rules are left-linear \item<4-> rewrite rule $\ell \to r$ is \alert<4>{right-linear} if $r$ is linear \item<5-> rewrite rule $\ell \to r$ is \alert<5>{linear} if $\ell$ and $r$ are linear \item<6-> TRS is (right-)linear if all rewrite rules are (right-)linear \end{itemize} \end{definitions} \bigskip \begin{examples}<7-> \begin{itemize} \item<7-> $\m{g}(\alert<7>x) \to \m{f} (\alert<7>{x},\m{g}(\alert<7>{x}))$ \\[.5ex] left-linear but not right-linear \item<8-> $\m{f}(\alert<8>{x},\alert<8>{x}) \to \m{a}$ \\[.5ex] right-linear but not left-linear \end{itemize} \end{examples} \end{frame}