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