\begin{frame}{Pumping Lemma for Regular Languages (1959)}
  \begin{block}{Pumping Lemma}
    Let $L$ be a regular language.
    There \alert{exists $m > 0$} such that
    \alert{every $w \in L$} with \alert{$|w| \geq m$}
    can be written in the form 
    \begin{talign}
      \alert{w = xyz}
    \end{talign}
    with \alert{$|xy| \leq m$} and \alert{$|y| \geq 1$}, and
    \alert{$xy^i z \in L$} for every $i \geq 0$.
  \end{block}
  \pause
  
  \begin{proof}
    We have $L = L(M)$ for some DFA $M$ with $m$ states.
    \pause\medskip
  
    When $M$ reads $w \in L$ with $|w|\geq m$, there must be a cycle
    \begin{center}
      \begin{tikzpicture}[default,node distance=20mm,->]
        \node (q0) [state] {}; \draw ($(q0) + (-10mm,0mm)$) -- (q0); 
        \node (q1) [state,right of=q0] {};
        \node (q2) [fstate,right of=q1] {};
        
        \draw (q0) to node [label,above] {$x$} (q1);
        \draw (q1) to node [label,above] {$z$} (q2);
        \draw (q1) to[tloop] node [label,above] {$y$} (q1);

        \begin{scope}[red]
        \node [label,inner sep=0] (t) at (50mm,10mm) {first repetition of a state};
        \draw (t) to[bend right=10] (q1);
        \end{scope}
      \end{tikzpicture}
    \end{center}    
    with $|xy| \leq m$ and $|y| \geq 1$. Then $xy^i z \in L$ for every $i \geq 0$.
  \end{proof}
\end{frame}