\begin{frame}{Turing Machine Computations}
    The \emph{computation steps $\vdash$} on configurations are defined by:
      v\alert{q}aw &\vdash vb\alert{q'}w 
        && \text{if }\delta(q,a) = (q',b,R) \\
      vc\alert{q}aw &\vdash v\alert{q'}cbw 
        && \text{if }\delta(q,a) = (q',b,L) 
    where $v,w \in \Gamma^*$, $a,c \in \Gamma$ and $q \in Q$.
  We write $\vdash^*$ for a computation of zero or more steps.
    Assume that ($\delta$ is undefined in all other case)
      \delta(q_0,a) &= (q_0,a,R) &
      \delta(q_1,a) &= (q_1,b,L) &
      \delta(q_0,\Box) &= (q_1,c,L)
    Then we have steps:
      q_0 aa 
      \mpause[1]{\vdash a q_0 a}
      \mpause{\vdash aa q_0}  
      \mpause{\vdash a q_1 ac}
      \mpause{\vdash q_1 abc}
      \mpause{\vdash q_1 \Box bbc}
    \mpause[3]{Here we use $aa q_0 \approx aa q_0 \Box$}\mpause[6]{ and $q_1 abc \approx \Box q_1 abc$.}
    A configuration $vqaw$ is a \emph{halting state} if $\delta(q,a) \text{ is undefined}$.