63/145
\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}