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