\begin{frame}[fragile]{From Context-Sensitive Grammars to LBA's}
  \begin{goal}{Theorem}
    For every context-sensitive grammar $G$ there exists an LBA $M$
    such that $L(M) = L(G)$.
  \end{goal}
  \pause\medskip
  
  \begin{proof}
    A derivation of $w \in L(G)$ contains only words of length $\leq |w|$.
    \medskip
    
    A nondeterministic Turing machine can simulate (guess)
    this derivation without leaving the bounds of $w$.
  \end{proof}
\end{frame}