\begin{frame}
  \small
  
  \begin{definitions}
  \begin{itemize}
  \item
    \alert<1-3>{abstract rewrite system} (\alert<1-3>{ARS}) is
    set $A$ equipped with binary relation $\to$
    \onslide<2->
    \begin{tabular}{@{}l@{\qquad}l@{}}
    \begin{minipage}[t]{3.5cm}
    \GREEN{
    \begin{tikzpicture}[on grid,baseline=3mm]
    \node (1)              {\alert<4-6>{$\e{\m{a}}$}};
    \node (2) [right=of 1] {\alert<4,6>{$\e{\m{b}}$}};
    \node (3) [right=of 2] {\alert<4>{$\e{\m{c}}$}};
    \node (4) [right=of 3] {$\e{\m{d}}$};
    \node (5) [below=of 2] {\alert<4,6>{$\e{\m{e}}$}};
    \node (6) [below=of 3] {\alert<4>{$\e{\m{f}}$}};
    \node (7) [below=of 6] {$\e{\m{g}}$};
    \alert<4,6>{
    \draw[->] (1) -- (5);
    }
    \alert<6>{
    \draw[->] (2) -- (1);
    }
    \alert<4>{
    \draw[->] (2) -- (3);
    }
    \draw[->] (3) -- (4);
    \alert<4>{
    \draw[->] (3) -- (6);
    }
    \alert<4,6>{
    \draw[->] (5) -- (2);
    }
    \draw[->] (5) -- (7);
    \draw[->] (6) -- (5);
    \draw[->] (6) -- (7);
    \end{tikzpicture}}
    \end{minipage} &
    \onslide<3->
    \begin{minipage}[t]{7cm}
    \bigskip
    \bigskip
    ARS $\AA = \ARS$
    \begin{itemize}
    \item
      $A = \{ \mG{a}, \mG{b}, \mG{c}, \mG{d}, \mG{e}, \mG{f}, \mG{g} \}$
      \smallskip
    \item
      ${\to} = \left\{\begin{array}{@{}l@{}}
      (\mG{a},\mG{e}), (\mG{b},\mG{a}),
      (\mG{b},\mG{c}), (\mG{c},\mG{d}),
      (\mG{c},\mG{f}) \\[.5ex]
      (\mG{e},\mG{b}), (\mG{e},\mG{g}),
      (\mG{f},\mG{e}), (\mG{f},\mG{g}) 
      \end{array}\right\}$
    \end{itemize}
    \end{minipage}
    \end{tabular}
  \item<4->
    \alert{rewrite sequence}
    \vspace{-1ex}
    \begin{itemize}
    \item
      \makebox[15mm][l]{\alert<4>{finite}}
      \makebox[50mm][l]{\GREEN{$\m{a} \to \m{e} \to \m{b} \to\onslide<5->{\callout{rewrite step}} \m{c} \to \m{f}$}}
      \makebox[20mm][l]{\onslide<8->{\alert<8>{length 4}}}
      \onslide<9->{\alert<9>{$a \to^* f$}}
    \item<6->
      \makebox[15mm][l]{\alert<5>{empty}}
      \makebox[50mm][l]{\GREEN{$\m{a}$}}
      \makebox[20mm][l]{\onslide<8->{\alert<8>{length 0}}}
      \onslide<9->{\alert<9>{$a \to^* a$}}
    \item<7->
      \makebox[15mm][l]{\alert<6>{infinite}}
      \makebox[50mm][l]{\GREEN{$\m{a} \to \m{e} \to \m{b} \to \m{a} \to \m{e} \to \m{b} \to \cdots$}}
      \onslide<8->{\alert<8>{length $\omega$}}
      \smallskip
    \end{itemize}
      \onslide<8->
      The \alert<8>{length} of a rewrite sequence is the number of rewrite steps.\\
      \onslide<9->
      We write \alert<9>{$x \to^* y$} if $x$ rewrites to $y$ in $0$ or more steps.
  \end{itemize}
  \end{definitions}

\end{frame}