\begin{frame}{DFAs Reading Words}
  Let $M = (Q,\Sigma,\delta,q_0,F)$ be a DFA. 
  \begin{block}{}
    A \emph{configuration} of $M$ is a pair $\alert{(q,w)}$ with $q \in Q$ and $w \in \Sigma^*$.
  \end{block}
  So $(q,w)$ means the automaton is in state $q$ and reads word $w$.

  \begin{block}{}
    The \emph{step relation $\vdash$} of $M$ is defined on configurations by 
    \begin{talign}
      \alert{(q,aw) \vdash (q',w)} \quad \text{if $\delta(q,a)=q'$}
    \end{talign}
  \end{block}
  \pause
  
  \begin{exampleblock}{}   
    \edfa
    Then  
    \(
      (q_0,abba) \vdash 
      \mpause[1]{ (q_0,bba) \vdash }
      \mpause{ (q_1,ba) \vdash }
      \mpause{ (q_0,a) \vdash }
      \mpause{ (q_0,\lambda). }
    \)
  \end{exampleblock}
  \pause\pause\pause\pause\pause
  
  \begin{block}{}
    We define $\alert{\vdash^*}$ as the \emph{reflexive transitive closure of $\vdash$}.
  \end{block}
  
  \begin{exampleblock}{}
    Continuing the above example, we have $(q_0,abba) \vdash^* (q_0,\lambda)$.
  \end{exampleblock}
\end{frame}