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}