\begin{frame}{From Final States to Acceptance with Empty Stack}
  \begin{exampleblock}{}
    Consider the NPDA $M$:
    \begin{center}
      \begin{tikzpicture}[default,node distance=25mm,->,s/.style={minimum size=5mm}]
        \node (q0) [state,s] {$q_0$}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \draw (q0) to[tloop] node [label,above] {$a[z/1]$} (q0);
        \draw (q0) to[bloop] node [label,below] {$a[1/11]$} (q0);

        \node (q1) [fstate,s,right of=q0] {$q_1$};
        \draw (q0) to node [label,above] {$b[1/\lambda]$} (q1);
        \draw (q1) to[tloop] node [label,above] {$b[1/\lambda]$} (q1);
      \end{tikzpicture}
      \vspace{-2ex}
    \end{center}
    Transform it into NPDA $N$ such that $L(M) = L(N) = L_\lambda(N)$\pause:
    \begin{center}
      \vspace{-1ex}
      \begin{tikzpicture}[default,node distance=22mm,->,s/.style={minimum size=5mm}]
        \mpause[1]{\node (q0') [state,s] {$\widehat{q_0}$}; \draw ($(q0') + (-8mm,0mm)$) -- (q0');}
        \node (q0) [state,s,right of=q0'] {$q_0$}; \draw ($(q0) + (-8mm,0mm)$) -- (q0); 
        \alt<-7>{ \node (q1) [fstate,s,right of=q0] {$q_1$}; }{ \node (q1) [state,s,right of=q0] {$q_1$}; }
        \mpause[1]{\node (qe) [state,s,right of=q1] {$q_e$};}
        \mpause[1]{
          \alt<-7>{ \node (qf) [state,s,right of=qe] {$q_f$}; }{ }
        }

        \mpause{\draw (q0') to node [label,above] {$\lambda[z/z\hat{z}]$} (q0);}
        \draw (q0) to[tloop] node [label,above] {$a[z/1]$} (q0);
        \draw (q0) to[bloop] node [label,below] {$a[1/11]$} (q0);

        \draw (q0) to node [label,above] {$b[1/\lambda]$} (q1);
        \draw (q1) to[tloop] node [label,above] {$b[1/\lambda]$} (q1);

        \mpause{\draw (q1) to node [label,below,align=center] {$\lambda[z/z]$\\$\lambda[\hat{z}/\hat{z}]$\\$\lambda[1/1]$} (qe);}
        \mpause{\draw (qe) to[tloop] node [label,above,align=center] {$\lambda[z/\lambda]$\\$\lambda[1/\lambda]$} (qe);}
        \mpause{\draw (qe) to node [label,above,align=center] {$\lambda[\hat{z}/\lambda]$} (qf);}
        \mpause{ \node (qf) [fstate,s,right of=qe] {$q_f$}; }
      \end{tikzpicture}
      \vspace{-1ex}
    \end{center}
    \mpause{%
    This NPDA $N$ reaches the final state $\iff$ the stack is empty.
    \\
    }
  \end{exampleblock}
\end{frame}

\themex{From Acceptance with Empty Stack To Final States}