\begin{frame}{($\Leftarrow$) From Regular Expressions to NFAs}
  \begin{construction}[$\Leftarrow$]
    For every regular expression $r$,
    we build an NFA $M$ such that
    \begin{itemize}\setlength{\itemsep}{0pt}
      \item $L(M) = L(r)$,
      \item $M$ has precisely one final and one (different) starting state
    \end{itemize}
    \pause
    We construct $M$ by induction (recursion) on $r$.
    \begin{center}\vspace{-1ex}
    \begin{tikzpicture}[default,node distance=12mm,->,s/.style={minimum size=5mm}]
      \begin{scope}
        \mpause[1]{
        \node (q0) [state,s] {}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \node (q1) [fstate,s,right of=q0] {};
        }
        \node [left of=q0,anchor=east,node distance=9mm] {$\emptyset$:};
      \end{scope}
  
      \begin{scope}[yshift=-16mm]
        \mpause{
        \node (q0) [state,s] {}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \node (q1) [fstate,s,right of=q0] {};
    
        \draw (q0) to node [above] {$\lambda$} (q1);
        }
        \node [left of=q0,anchor=east,node distance=9mm] {$\lambda$:};
      \end{scope}
  
      \begin{scope}[yshift=-32mm]
        \mpause{
        \node (q0) [state,s] {}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \node (q1) [fstate,s,right of=q0] {};
    
        \draw (q0) to node [above] {$a$} (q1);
        }
        \node [left of=q0,anchor=east,node distance=9mm] {$a$:};
      \end{scope}
  
      \begin{scope}[xshift=45mm,yshift=-0mm]
        \mpause{
        \node (q0) [state,s] {}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \subnfa{r_1}{$(q0)+(10mm,5mm)$}
        \subnfa{r_2}{$(q0)+(10mm,-5mm)$}
        \node (qf) at ($(r_1f)!0.5!(r_2f) + (10mm,0mm)$) [fstate,s] {}; 
    
        \draw (q0) to node [above,pos=.4] {$\lambda$} (r_1s);
        \draw (q0) to node [below,pos=.4] {$\lambda$} (r_2s);
        \draw (r_1f) to node [above,pos=.4] {$\lambda$} (qf);
        \draw (r_2f) to node [below,pos=.4] {$\lambda$} (qf);
        }    
        \node [left of=q0,anchor=east,node distance=9mm] {$r_1 + r_2$:};
      \end{scope}
  
      \begin{scope}[xshift=45mm,yshift=-16mm]
        \mpause{
        \subnfa{r_1}{$(0mm,0mm)$} 
        \draw ($(r_1s) + (-8mm,0mm)$) -- (r_1s);
        \subnfafinal{r_2}{$(r_1f)+(10mm,0mm)$}
         
        \draw (r_1f) to node [above,pos=.4] {$\lambda$} (r_2s);
        }    
        \node [left of=r_1s,anchor=east,node distance=9mm] {$r_1 \cdot r_2$:};
      \end{scope}
  
      \begin{scope}[xshift=45mm,yshift=-32mm]
        \mpause{
        \node (q0) [state,s] {}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \subnfa{r}{$(q0)+(10mm,0mm)$}
        \node (qf) at ($(rf) + (10mm,0mm)$) [fstate,s] {}; 
    
        \draw (q0) to node [above,pos=.4] {$\lambda$} (rs);
        \draw (rf) to node [above,pos=.4] {$\lambda$} (qf);
    
        \draw (q0) to[out=70,in=120,looseness=.4] node [above,label] {$\lambda$} (qf);
        \draw (qf) to[out=180+60,in=180+130,looseness=.4] node [below,label] {$\lambda$} (q0);
        }  
        \node [left of=q0,anchor=east,node distance=9mm] {$r^*$:};
      \end{scope}
      \end{tikzpicture}
    \end{center}\vspace{-2ex}
  \end{construction}
\end{frame}