\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}