\begin{frame}
  \small
  
  \begin{block}{}
  \begin{center}
  rewrite \alert<1>{sequence} $A\colon s \to^* t$
  \qquad
  set of positions $Q \subseteq \Pos(s)$
  \end{center}
  \end{block}
  \smallskip
  
  \begin{definition}[Descendants after Rewrite Sequence]
  \smallskip
  The descendants of $Q$ after $A$ in $t$
  \[
  Q \project A = \begin{cases}
  Q & \text{if $A$ is empty sequence} \\
  (Q \project A_1) \project A_2
  & \text{If $A = A_1; A_2$ with $A_1\colon s \to u$ and
  $A_2\colon u \to^* t$}
  \end{cases}
  \]
  \end{definition}
  \medskip\pause
  
  \begin{lemma}
  \makebox[35mm][l]{For left-linear TRSs:}
  if $Q$ is parallel (\,$\forall\:p \neq q \in Q \colon p \parallel q$)
  then so is $Q \project A$.
  \end{lemma}
  \pause
  
  \begin{lemma}
  \makebox[35mm][l]{For orthogonal TRSs:}
  if $Q$ is set of redex positions then so is $Q \project A$.
  \end{lemma}
  \pause

  \begin{block}{Terminology}
  \smallskip
  A descendant of redex is called \alert{residual}.
  \smallskip
  \end{block}
\end{frame}