\begin{frame} \frametitle{Complexity of Confluence} \small \begin{theorem} $CR(\atrs)$ is $\cpi{0}{2}$-complete. \end{theorem} \pause \begin{proof} We extend $H_M$ with: \vspace{-1.5ex} \begin{align*} S(x,\tmiblank) &\to T \\ S(\tmiblank,y) &\to q_0(\tmiblank,y) \\ S(x,s(y)) &\to S(s(x),y) \\ S(s(x),y) &\to S(x,s(y)) \end{align*} \vspace{-4ex} \noindent\pause Then $$T \from S(u,\tmiblank) \conv S(\tmiblank,v) \to q_0(\tmiblank,v)$$ if and only if $u = v = s^n(\tmiblank)$ for some $n \in \NN$.\\ \pause\smallskip Hence $CR(\atrs)$ holds\\ \smallskip \quad $\Longleftrightarrow$ $q_0(\tmiblank,s^n(\tmiblank)) \to^* T$ for all $n \in \NN$\\ \quad $\Longleftrightarrow$ $M$ is total. \smallskip \end{proof} \end{frame} \againframe{tower}