\begin{frame}
  \small

  \begin{definition}[Term Rewriting]
  \smallskip
  Let $\atrs = \TRS$ be a TRS. The \alert{rewrite relation $\to_\atrs$} on $\TT(\FF,\VV)$ is defined as:
  \begin{align*}
    C[\ell \sigma] \to_\atrs C[r \sigma] 
  \end{align*}
  for every:
  \begin{itemize}
    \item rule $\ell \to r \in \RR$,
    \item context $C$, and
    \item substitution $\sigma$.
  \end{itemize}
  \smallskip
  Let $p$ be the position of $\Box$ in $C$.
  Then we say that the rewrite step is at position $p$.\\
  \smallskip
  \end{definition}
  
  \onslide<2->
  \begin{example}
    The rule $\m{add}(\m{0},y) \to y$ with $y \mapsto \m{s}(0)$
    and $C = \m{add}(0,\Box)$ gives rise to the step:
    \begin{align*}
      \m{add}(0,\m{add}(\m{0},\m{s}(0)))
      \to 
      \m{add}(0,\m{s}(0))
    \end{align*}
    at position $2$.
  \end{example}
\end{frame}