\begin{frame}
  \small
  
  \begin{example}
  \smallskip
  TRS $\RR$ modeling \alert{Sieve of Eratostheness} for generating
  list of prime numbers
  \[
  \GREEN{\begin{array}[t]{@{}r@{~}c@{~}l@{\hspace{-5mm}}r@{~}c@{~}l@{}}
  \m{primes} & \to & \m{sieve}(\m{from}(\m{s}(\m{s}(\m{0})))) &
  \m{sieve}(\m{0}:y) & \to & \m{sieve}(y) \\[.5ex]
  \m{from}(x) & \to & x:\m{from}(\m{s}(x)) &
  \m{sieve}(\m{s}(x):y) & \to &
  \m{s}(x):\m{sieve}(\m{filter}(x,y,x)) \\[.5ex]
  \m{head}(x:y) & \to & x &
  \m{filter}(\m{0},y:z,w) & \to & \m{0}:\m{filter}(w,z,w) \\[.5ex]
  \m{tail}(x:y) & \to & y &
  \m{filter}(\m{s}(x),y:z,w) & \to & y:\m{filter}(x,z,w)
  \end{array}}
  \]
  
  \vspace{-2ex}
  
  \begin{itemize}
  \item<2->
  $\RR$ is confluent but not terminating
  \[
  \GREEN{
  \m{from(0)}
  \to \m{0}:\m{from(s(0))}
  \to \m{0}:\m{(s(0)}:\m{from(s(s(0))))}
  \to \cdots
  }
  \]
  \vspace{-4ex}
  \item<3->
  \makebox[6cm][l]{how to prove confluence of $\RR$ ?}
  \onslide<4->{\makebox[25mm][l]{\alert{orthogonality}}
  (lecture 8)}
  \item<5->
  $\exists$ non-terminating terms with (unique) normal form
  \[
  \GREEN{
  \m{head(tail(tail(primes)))} \to^! \m{s(s(s(s(s(0)))))}
  }
  \]
  \vspace{-4ex}
  \item<6->
  \makebox[6cm][l]{how to compute normal forms in $\RR$ ?}
  \onslide<7->{\makebox[25mm][l]{\alert{strategy}}
  (lecture 9)}
  \end{itemize}
  \end{example}

\end{frame}