\begin{frame}[label=complete developments]
  \small
  
  %AM 23.06 QUESTION is this true for non-orthogonal TRSs ?!
  \begin{theorem}
  \smallskip
  Developments are \alert<1>{finite}.
  \end{theorem}
  
  \medskip
  
  \begin{definition}<2->
  \smallskip
  A development $A\colon s \to^* t$ of %set of redex positions
  $Q \subseteq \Pos(s)$ is \alert{complete} if
  $Q \project A = \varnothing$.
  \pause\smallskip
  
  We write \alert{$s \dev t$} (called \alert{multi-step}) if there is a complete development $s \to^* t$.
  \end{definition}
  
  \medskip\pause
  \begin{example}
  \vspace{-1ex}
  \GREEN{
  \begin{alignat*}{2}
  \underline{\m{s}(\m{0}) \alert{\times} (\m{0} \alert{\times} \m{0})}
  &\to (\m{0} \times \underline{(\m{0} \alert{\times} \m{0})}) + (\m{0} \alert{\times} \m{0})
  \to (\m{0} \times \m{0}) + (\m{0} \alert{\times} \m{0})
  &\qquad&\huil
  \\
  \onslide<3->{\m{s}(\m{0}) \alert{\times} \underline{(\m{0} \alert{\times} \m{0})}}
  &\onslide<3->{\to \underline{\m{s}(\m{0}) \alert{\times} \m{0}}
  \to (\m{0} \times \m{0}) + \m{0}}
  && \onslide<3->{\lach}
  \end{alignat*}}
  \vspace{-3ex}
  \end{example}
  
  
%   %AM 22.06 QUESTION is this true ?!
%   \begin{lemma}<3->
%   \smallskip
%   for orthogonal TRSs: ~
%   $s \to^* t$ is complete development \quad$\iff$\quad $s \dev t$
%   \end{lemma}
  
  \medskip
  
  \begin{theorem}<4->
  \smallskip
  All complete developments of $Q$ are \alert<4>{permutation equivalent}.
  \end{theorem}
\end{frame}