\begin{frame}
  \small

  \begin{definition}[From Turing Machines to Term Rewriting Systems]
  For a Turing machine $M = \langle Q, q_0, F, \Sigma, \Box, \delta \rangle$ we define
  a TRS $\atrs_M$ as follows:
  \begin{align*}
    \bfunap{\astate}{x}{\funap{f}{y}} &\to \bfunap{\astate'}{\funap{f'}{x}}{y}
    &&\text{ for every }\tmtrans{\astate}{f} = \triple{\astate'}{f'}{\tmR}\\
    \bfunap{\astate}{\funap{g}{x}}{\funap{f}{y}} &\to \bfunap{\astate'}{x}{\funap{g}{\funap{f'}{y}}}
    &&\text{ for every }\tmtrans{\astate}{f} = \triple{\astate'}{f'}{\tmL}
  \end{align*}
  \pause
  together with four rules for `extending the tape':
  \vspace{-1ex}
  \begin{align*}
    \bfunap{\astate}{\tmiblank}{\funap{f}{y}} &\to \bfunap{\astate'}{\tmiblank}{\tmblank{\funap{f'}{y}}}
    &&\text{ for every }\tmtrans{\astate}{f} = \triple{\astate'}{f'}{\tmL}\\
    \bfunap{\astate}{x}{\tmiblank} &\to \bfunap{\astate'}{\funap{f'}{x}}{\tmiblank}
    &&\text{ for every }\tmtrans{\astate}{\stmblank} = \triple{\astate'}{f'}{\tmR}\\
    \bfunap{\astate}{\funap{g}{x}}{\tmiblank} &\to \bfunap{\astate'}{x}{\funap{g}{\funap{f'}{\tmiblank}}}
    &&\text{ for every }\tmtrans{\astate}{\stmblank} = \triple{\astate'}{f'}{\tmL}\\
    \bfunap{\astate}{\tmiblank}{\tmiblank} &\to \bfunap{\astate'}{\tmiblank}{\tmblank{\funap{f'}{\tmiblank}}}
    &&\text{ for every }\tmtrans{\astate}{\stmblank} = \triple{\astate'}{f'}{\tmL}
  \end{align*}
  \end{definition}
\end{frame}