25/40
\begin{frame}
  \frametitle{Complexity of (Weak) Normalization}
  \small

  As a consequence we obtain:
  
  \begin{theorem}
  $SN(\atrs,t)$ and $WN(\atrs,t)$ of single terms are $\csig{0}{1}$-complete.
  \end{theorem}
  \pause
  \begin{proof}
  The term $t = q_0(\tmiblank,\tmiblank)$ is normalizing in $\atrs_M$ $\Longleftrightarrow$ $M$ halts on the blank tape.\\
  Moreover $SN(t) \Longleftrightarrow WN(t)$ since every reduct contains at most one redex.
  \end{proof}
  \pause\bigskip
  
  \begin{theorem}
  $SN(\atrs)$ and $WN(\atrs)$ are $\cpi{0}{2}$-complete.
  \end{theorem}
\end{frame}