87/145
\begin{frame}
  \small
  
  \begin{block}{}
  \begin{center}
  rewrite step $A\colon s \xrightarrow[\ell \to r]{p} t$
  at position $p \in \Pos(s)$ \quad\quad
  set of positions $Q \subseteq \Pos(s)$
  \end{center}
  \end{block}
  
  \bigskip
  
  \begin{definition}[Descendants after Rewrite Step]
  \smallskip
  \begin{itemize}
  \item
  The \alert{descendants} of $q$ after $A$ in $t$
  \[
  \alert{q \project A} = \begin{cases}
  \{ q \} & \text{if $q < p$ or $q \parallel p$} \\
  \{ p p_3 p_2 \mid r|_{p_3} = \ell|_{p_1} \} &
  \text{if $q = p \ct p_1 \ct p_2$ with $p_1 \in \Pos_\VV(\ell)$} \\
  \varnothing & \text{otherwise}
  \end{cases}
  \]
  \item<2->
  The descendants of $Q$ after $A$ in $t$ are
  \[
  \alert{Q \project A} = \bigcup_{q \in Q} q \project A
  \]
  \end{itemize}
  \end{definition}
  
  \bigskip
  
  %AM something to ask during the lecture, to practice during the exercises,
  %   but (perhaps) not to put on slide
  % \begin{block}{Question}
  % What are the possibilites for `otherwise'?
  % \end{block}
  
  %AM 21.06 TODO add (abstract) picture
\end{frame}