\begin{frame}
  \frametitle{Observations on $\atrs_M$}
  \small
  
  \begin{lemma}
  For every Turing machine $M$, the TRS $\atrs_M$ is orthogonal.
  \end{lemma}
  \pause\medskip

  \begin{theorem}
  A Turing machine $M$ halts on $w$ if and only if $q_0(\tmiblank,w(\tmiblank))$ terminates in $\atrs_M$.
  \end{theorem}
  \pause\medskip

  \begin{theorem}
  A Turing machine $M$ halts on all configurations if and only if $\atrs_M$ terminates.
  \end{theorem}
  
\end{frame}