\begin{frame}{From Turing Machines to Unrestricted Grammars}
  \begin{goal}{Theorem}
    For every TM $M$ there is a grammar $G$ with $L(G) = L(M)$.
  \end{goal}
  \pause
  
  \begin{construction}
    The variables are $S,T,\alert{\Box}$\\
    \ \hfill and $V_\gamma^\alpha,V_{q\gamma}^\alpha$ for every $\alpha \in \Sigma \cup \{\Box\}$, $\gamma \in \Gamma$ and $q\in Q$.
    \pause\medskip

    \emph{Step 1}: guessing the word $w$
    \begin{talign}
      S &\to V_\Box^\Box S \mid S V_\Box^\Box\mid T \\[-.25ex]
      T &\to T V_a^a \mid V_{q_0a}^a &&\text{for every } a \in \Sigma 
    \end{talign}
    \pause
    After step 1, we have derived something of the form
    \begin{talign}
      V^\Box_\Box \cdots V^\Box_\Box  
      V^{a_1}_{\alert{q_0}a_1} V^{a_2}_{a_2} V^{a_3}_{a_3} \cdots V^{a_n}_{a_n}
      V^\Box_\Box \cdots V^\Box_\Box  
    \end{talign}
    where $w = a_1a_2 \cdots a_n$.
    \pause\medskip
    
    Next, the TM is simulated using the lower line (the subscripts).
  \end{construction}
\end{frame}