\begin{frame}
  \begin{definition}[Redex occurrence]
  A \alert{redex occurrence} in a term $t$ 
  is a pair $\langle p,\;\ell \to r \rangle$ such that
  \begin{itemize}
    \item $\ell \to r \in R$, and
    \item $\ell$ matches $t|_p$.
  \end{itemize}
  We write $s \mathrel{\stackrel{r} {\to}} t$ if $r$ is the redex occurrence
  contracted in the step $s \to t$.
  \end{definition}
  
  \begin{definition}[Pattern]
  The \alert{pattern} of a redex occurrence $\langle p,\;\ell \to r \rangle$ in $t$
  are the symbol occurrences
  in $t$ at positions $pq$ with $q \in \Pos_\FF(\ell)$ a non-variable position in $\ell$.
  \end{definition}
  
  \begin{definition}[Overlap]
  Two redex occurrences:
  \begin{itemize}
    \item \alert{overlap} if their pattern share at least one symbol occurrence,
    \item are \alert{parallel} if their positions are parallel, and
    \item are \alert{nested} if they are not parallel and do not overlap.
  \end{itemize} 
  \end{definition}
\end{frame}