35/40
\begin{frame}
  \frametitle{Complexity of Confluence}
  \small
  
  \begin{definition}
  For a Turing machine $M$ we define $H_M$ to be $\atrs_M$ extended with:
  \vspace{-1ex}
  \begin{align*}
  \bfunap{\astate}{x}{\funap{f}{y}} &\to \tmT 
    && \mbox{for every $f \in \Sigma, \astate \in \tmstates$ with $\tmtrans{\astate}{f}$ is undefined} \\
  \bfunap{\astate}{x}{\tmiblank} &\to \tmT 
    && \mbox{for every $\astate \in \tmstates$ with $\tmtrans{\astate}{\stmblank}$ is undefined}
  \end{align*}
  \end{definition}
  \pause

  \begin{theorem}
  $CR(\atrs,t)$ for single terms is $\cpi{0}{2}$-complete.
  \end{theorem}
  \pause
  
  \begin{proof}
  We extend $H_M$ with:
  \vspace{-1.5ex}
  \begin{align*}
    S(x) &\to T &
    S(x) &\to S(s(x)) &
    S(x) &\to q_0(\tmiblank,x)
  \end{align*}
  \vspace{-4ex}
  
  \noindent\pause
  Then $T \from S(0(\tmiblank)) \to^* S(s^n(0(\tmiblank))) \to q_0(\tmiblank,s^n(0(\tmiblank)))$ for all $n \in \NN$.\\
  \pause\smallskip
  
  Hence $CR(\atrs,S(0(\tmiblank)))$ holds\\
  \quad $\Longleftrightarrow$ $q_0(\tmiblank,s^n(0(\tmiblank))) \to^* T$ for all $n \in \NN$\\
  \quad $\Longleftrightarrow$ $M$ is total.
  \end{proof}
\end{frame}