
diff -r 813e7257c7c3 -r d47c2143ab8a Slides/Slides4.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/Slides/Slides4.thy	Wed Feb 22 13:25:49 2012 +0000
@@ -0,0 +1,1382 @@
+(*<*)
+theory Slides4
+imports "~~/src/HOL/Library/LaTeXsugar"
+begin
+
+notation (latex output)
+  set ("_") and
+  Cons  ("_::/_" [66,65] 65) 
+
+(*>*)
+
+
+text_raw {*
+  \renewcommand{\slidecaption}{Edinburgh, 21 February 2012}
+  \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        
+  \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]
+  \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}
+  \frametitle{%
+  \begin{tabular}{@ {}c@ {}}
+  \LARGE Formalising\\[-3mm] 
+  \LARGE Regular Language Theory\\[-3mm] 
+  \LARGE with Regular Expressions,\\[-3mm] 
+  \LARGE \alert<2>{Only}\\[0mm] 
+  \end{tabular}}
+  
+  \begin{center}
+   Christian Urban\\
+  \small King's College London
+  \end{center}\bigskip
+ 
+  \begin{center}
+  \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA
+  University of Science and Technology in Nanjing
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{}
+
+  \mbox{}\\[-10mm]
+  \begin{itemize}
+  \item My background is in 
+  \begin{itemize}
+  \item \normalsize theorem provers
+  \item \normalsize develop Nominal Isabelle
+  \end{itemize}\bigskip\bigskip  
+
+  \item<1->to formalise and mechanically check proofs from 
+  programming language research and TCS\bigskip
+
+  \item<2->our biggest success story \ldots 
+  \end{itemize}
+  
+  \only<1->{
+  \begin{textblock}{6}(10.9,3.5)
+  \includegraphics[scale=0.23]{isabelle1.png}
+  \end{textblock}}
+  
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{}
+
+  \begin{tabular}{c@ {\hspace{2mm}}c}
+  \\[6mm]
+  \begin{tabular}{c}
+  \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]
+  {\footnotesize Bob Harper}\\[-2.5mm]
+  {\footnotesize (CMU)}
+  \end{tabular}
+  \begin{tabular}{c}
+  \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]
+  {\footnotesize Frank Pfenning}\\[-2.5mm]
+  {\footnotesize (CMU)}
+  \end{tabular} &
+
+  \begin{tabular}{p{6cm}}
+  \raggedright
+  \color{gray}{published a proof in\\ {\bf ACM Transactions on Computational Logic}, 2005,
+  $\sim$31pp}
+  \end{tabular}\\
+
+  \pause
+  \\[0mm]
+  
+  \begin{tabular}{c}
+  \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 
+  {\footnotesize Andrew Appel}\\[-2.5mm]
+  {\footnotesize (Princeton)}
+  \end{tabular} &
+
+  \begin{tabular}{p{6cm}}
+  \raggedright
+  \color{gray}{relied on their proof in a\\ {\bf security} critical application}
+  \end{tabular}
+  \end{tabular}
+
+  
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+text {*
+  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+  \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 
+                     draw=black!50, top color=white, bottom color=black!20]
+  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
+                     draw=red!70, top color=white, bottom color=red!50!black!20]
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<2->[squeeze]
+  \frametitle{} 
+  
+  \begin{columns}
+  
+  \begin{column}{0.8\textwidth}
+  \begin{textblock}{0}(1,2)
+
+  \begin{tikzpicture}
+  \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]
+  { \&[-10mm] 
+    \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&
+    \node (proof1) [node1] {\large Proof}; \&
+    \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\
+    
+    \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&
+    \onslide<4->{\node (proof2) [node1] {\large Proof};} \&
+    \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+     
+    \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+    \onslide<5->{\node (proof3) [node1] {\large Proof};} \&
+    \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\
+
+    \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&
+    \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&
+    \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&
+    \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\
+  };
+
+  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+  \draw[->,black!50,line width=2mm] (proof1) -- (alg1);
+  
+  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}
+  \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}
+
+  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}
+  \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}
+  
+  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}
+  \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}
+
+  \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 
+  \end{tikzpicture}
+
+  \end{textblock}
+  \end{column}
+  \end{columns}
+
+
+  \begin{textblock}{3}(12,3.6)
+  \onslide<4->{
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};
+  \end{tikzpicture}}
+  \end{textblock}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{}
+
+  \begin{itemize}
+  \item I also found fixable errors in my Ph.D.-thesis about cut-elimination
+  (examined by Henk Barendregt and Andy Pitts)
+  \item flaws in PIP (OS); a theorem without a shred of evidence (algorithms)
+  \end{itemize}\bigskip\bigskip
+
+
+  {\bf Conclusion:}\smallskip
+
+  Pencil-and-paper proofs in TCS are not foolproof, 
+  not even expertproof.
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\begin{tabular}{@ {}c@ {}}
+  \large Nipkow about Teaching Proofs in TCS:\hspace{3cm}\mbox{}\\[-4mm]
+  \large \textcolor{red}{``London Underground Phenomenon''}\\[-18mm]\mbox{}
+  \end{tabular}}
+
+  \begin{center}
+  \begin{tabular}{ccc}
+  students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs
+  \end{tabular}
+  \end{center}
+
+  \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{}
+  \begin{center}
+  \begin{block}{}
+  \color{gray}
+  \small
+  ``I still remember having to grade hundreds of exams where the
+  students started out by assuming what had to be proved, or filled
+  page after page with gibberish in the hope that, somewhere in the
+  mess, they might accidentally have said something
+  correct. \ldots{}innumerable examples of ``parrot proofs'' ---
+  NP-completeness reductions done in the wrong direction, arguments
+  that look more like LSD trips than coherent chains of logic \ldots{}''
+  \end{block}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{}
+
+  \begin{itemize}
+  \item part of the problem is teaching the obvious\medskip
+  \begin{center}
+  \smath{\infer{A \vdash A}{}}
+  \end{center}\bigskip\bigskip
+  \item teach proofs, not logic
+  \item students having too little practice and no good literature for how to do proofs\\
+  \textcolor{gray}{\small(Velleman is too mathematics oriented)}
+  \bigskip\bigskip\pause
+
+  \item proof assistants lead to abundant practice because they are 
+  addictive like video games (Nipkow, Pierce)\\
+   \textcolor{gray}{\small(in the past they were just frustrating, but they got much better)}
+  \end{itemize}
+
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+  \frametitle{Regular Expressions}
+
+  \begin{textblock}{6}(2,4)
+  \begin{tabular}{@ {}rrl}
+  \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\
+         & \bl{$\mid$} & \bl{[]}\\
+         & \bl{$\mid$} & \bl{c}\\
+         & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\
+         & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\
+         & \bl{$\mid$} & \bl{r$^*$}\\
+  \end{tabular}
+  \end{textblock}
+
+  \begin{textblock}{6}(8,3.5)
+  \includegraphics[scale=0.35]{Screen1.png}
+  \end{textblock}
+
+  \begin{textblock}{6}(10.2,2.8)
+  \footnotesize Isabelle:
+  \end{textblock}
+
+  \begin{textblock}{6}(7,12)
+  \footnotesize\textcolor{gray}{students have seen them and can be motivated about them}
+  \end{textblock}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[t]
+
+  \mbox{}\\[-2mm]
+
+  \small
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}
+  \bl{nullable (NULL)}            & \bl{$=$} & \bl{false} &\\
+  \bl{nullable (EMPTY)}           & \bl{$=$} & \bl{true}  &\\
+  \bl{nullable (CHAR c)}           & \bl{$=$} & \bl{false} &\\
+  \bl{nullable (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ 
+  \bl{nullable (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\
+  \bl{nullable (STAR r)}          & \bl{$=$} & \bl{true} & \\
+  \end{tabular}\medskip\pause
+
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}
+  \bl{der c (NULL)}            & \bl{$=$} & \bl{NULL} & \\
+  \bl{der c (EMPTY)}           & \bl{$=$} & \bl{NULL} & \\
+  \bl{der c (CHAR d)}           & \bl{$=$} & \bl{if c $=$ d then EMPTY else NULL} & \\
+  \bl{der c (ALT r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (der c r$_1$) (der c r$_2$)} & \\
+  \bl{der c (SEQ r$_1$ r$_2$)} & \bl{$=$} & \bl{ALT (SEQ (der c r$_1$) r$_2$)} & \\
+       &          & \bl{\phantom{ALT} (if nullable r$_1$ then der c r$_2$ else NULL)}\\
+  \bl{der c (STAR r)}          & \bl{$=$} & \bl{SEQ (der c r) (STAR r)} &\smallskip\\\pause
+
+  \bl{derivative [] r}     & \bl{$=$} & \bl{r} & \\
+  \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\
+  \end{tabular}\medskip
+
+  \bl{matches r s $=$ nullable (derivative s r)}
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
+  \mbox{}\\[-15mm]\mbox{}
+
+  \begin{center}
+  \huge\bf\textcolor{gray}{in Theorem Provers}\\
+  \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}
+  \end{center}
+
+  \begin{itemize}
+  \item automata @{text "\<Rightarrow>"} graphs, matrices, functions
+  \item<2-> combining automata / graphs
+
+  \onslide<2->{
+  \begin{center}
+  \begin{tabular}{ccc}
+  \begin{tikzpicture}[scale=1]
+  %\draw[step=2mm] (-1,-1) grid (1,1);
+  
+  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+
+  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  
+  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+  \draw (-0.6,0.0) node {\small$A_1$};
+  \draw ( 0.6,0.0) node {\small$A_2$};
+  \end{tikzpicture}}
+
+  & 
+
+  \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}}
+
+  &
+
+  \onslide<3->{\begin{tikzpicture}[scale=1]
+  %\draw[step=2mm] (-1,-1) grid (1,1);
+  
+  \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);
+  \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);
+
+  \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  
+  \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+
+  \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};
+  
+  \draw [very thick, red] (C) to [bend left=45] (B);
+  \draw [very thick, red] (D) to [bend right=45] (B);
+
+  \draw (-0.6,0.0) node {\small$A_1$};
+  \draw ( 0.6,0.0) node {\small$A_2$};
+  \end{tikzpicture}}
+
+  \end{tabular}
+  \end{center}\medskip
+
+  \only<4-5>{
+  \begin{tabular}{@ {\hspace{-5mm}}l@ {}}
+  disjoint union:\\[2mm]
+  \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}}
+  \end{tabular}}
+  \end{itemize}
+
+  \only<5>{
+  \begin{textblock}{13.9}(0.7,7.7)
+  \begin{block}{}
+  \medskip
+  \begin{minipage}{14cm}\raggedright
+  Problems with definition for regularity:\bigskip\\
+  \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
+  \medskip
+
+  \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}
+
+  \only<7->{You have to \alert{rename} states!}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
+  \mbox{}\\[-15mm]\mbox{}
+
+  \begin{center}
+  \huge\bf\textcolor{gray}{in Theorem Provers}\\
+  \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}
+  \end{center}
+
+  \begin{itemize}
+  \item Kozen's paper proof of Myhill-Nerode:\\ 
+  requires absence of \alert{inaccessible states}
+  \item complementation of automata only works for \alert{complete} automata
+  (need sink states)\medskip
+  \end{itemize}\bigskip\bigskip
+
+  \begin{center}
+  \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}
+  \end{center}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{}
+  \mbox{}\\[25mm]\mbox{}
+
+  \begin{textblock}{13.9}(0.7,1.2)
+  \begin{block}{}
+  \begin{minipage}{13.4cm}\raggedright
+  {\bf Definition:}\smallskip\\
+  
+  A language \smath{A} is \alert{regular}, provided there exists a\\ 
+  \alert{regular expression} that matches all strings of \smath{A}.
+  \end{minipage}
+  \end{block}
+  \end{textblock}\pause
+  
+  {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause
+
+  Infrastructure for free. But do we lose anything?\medskip\pause
+
+  \begin{minipage}{1.1\textwidth}
+  \begin{itemize}
+  \item pumping lemma\pause
+  \item closure under complementation\pause
+  \item \only<6>{regular expression matching}%
+       \only<7->{\sout{regular expression matching}
+  {\footnotesize(@{text "\<Rightarrow>"}Brozowski'64, Owens et al '09)}}
+  \item<8-> most textbooks are about automata
+  \end{itemize}
+  \end{minipage}
+
+  
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE The Myhill-Nerode Theorem}
+
+  \begin{itemize}
+  \item provides necessary and suf\!ficient conditions\\ for a language 
+  being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip
+
+  \item key is the equivalence relation:\medskip
+  \begin{center}
+  \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
+  \end{center}
+  \end{itemize}
+
+ 
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE The Myhill-Nerode Theorem}
+
+  \begin{center}
+  \only<1>{%
+  \begin{tikzpicture}[scale=3]
+  \draw[very thick] (0.5,0.5) circle (.6cm);
+  \end{tikzpicture}}%
+  \only<2->{%
+  \begin{tikzpicture}[scale=3]
+  \draw[very thick] (0.5,0.5) circle (.6cm);
+  \clip[draw] (0.5,0.5) circle (.6cm);
+  \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
+  \end{tikzpicture}}
+  \end{center}
+  
+  \begin{itemize}
+  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
+  \end{itemize}
+
+  \begin{textblock}{5}(2.1,5.3)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=2cm]
+  {$U\!N\!IV$};
+  \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}
+
+  \only<2->{%
+  \begin{textblock}{5}(9.1,7.2)
+  \begin{tikzpicture}
+  \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
+  {@{text "\<lbrakk>s\<rbrakk>"}$_{\approx_{A}}$};
+  \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \only<3->{
+  \begin{textblock}{11.9}(1.7,3)
+  \begin{block}{}
+  \begin{minipage}{11.4cm}\raggedright
+  Two directions:\medskip\\
+  \begin{tabular}{@ {}ll}
+  1.)\;finite $\Rightarrow$ regular\\
+  \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm]
+  2.)\;regular $\Rightarrow$ finite\\
+  \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
+  \end{tabular}
+
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE Initial and Final {\sout{\textcolor{gray}{States}}}}
+
+  \begin{textblock}{8}(10, 2)
+  \textcolor{black}{Equivalence Classes}
+  \end{textblock}
+
+
+  \begin{center}
+  \begin{tikzpicture}[scale=3]
+  \draw[very thick] (0.5,0.5) circle (.6cm);
+  \clip[draw] (0.5,0.5) circle (.6cm);
+  \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
+  \only<2->{\draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);}
+  \only<3->{\draw[red, fill] (0.2, 0.2) rectangle (0.4, 0.4);
+  \draw[red, fill] (0.4, 0.8) rectangle (0.6, 1.0);
+  \draw[red, fill] (0.6, 0.0) rectangle (0.8, 0.2);
+  \draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);}
+  \end{tikzpicture}
+  \end{center}
+
+  \begin{itemize}
+  \item \smath{\text{finals}\,A\,\dn \{[\!|s|\!]_{\approx_{A}}\;|\;s \in A\}}
+  \smallskip
+  \item we can prove: \smath{A = \bigcup \text{finals}\,A}
+  \end{itemize}
+
+  \only<2->{%
+  \begin{textblock}{5}(2.1,4.6)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=blue,text=white, minimum height=2cm]
+  {$[] \in X$};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \only<3->{%
+  \begin{textblock}{5}(10,7.4)
+  \begin{tikzpicture}
+  \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
+  {a final};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<-1>[c]
+  \frametitle{\begin{tabular}{@ {}l}\LARGE% 
+  Transitions between Eq-Classes\end{tabular}}
+
+  \begin{center}
+  \begin{tikzpicture}[scale=3]
+  \draw[very thick] (0.5,0.5) circle (.6cm);
+  \clip[draw] (0.5,0.5) circle (.6cm);
+  \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);
+  \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);
+  \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);
+  \draw[white] (0.1,0.7) node (X) {$X$};
+  \draw[white] (0.9,0.5) node (Y) {$Y$};
+  \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y);
+  \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {};
+  \end{tikzpicture}
+  \end{center}
+
+  \begin{center}
+  \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}
+  \end{center}
+
+  \onslide<8>{
+  \begin{tabular}{c}
+  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
+  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+  \node[state,initial] (q_0) {$R_1$};
+  \end{tikzpicture}
+  \end{tabular}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE Systems of Equations}
+
+  Inspired by a method of Brzozowski\;'64:\bigskip\bigskip
+
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-20mm}}c}
+  \\[-13mm]
+  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]
+  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+
+  %\draw[help lines] (0,0) grid (3,2);
+
+  \node[state,initial]   (p_0)                  {$X_1$};
+  \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};
+
+  \path[->] (p_0) edge [bend left]   node        {a} (p_1)
+                  edge [loop above]   node       {b} ()
+            (p_1) edge [loop above]   node       {a} ()
+                  edge [bend left]   node        {b} (p_0);
+  \end{tikzpicture}\\
+  \\[-13mm]
+  \end{tabular}
+  \end{center}
+
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+  & \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
+  & \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\
+  \end{tabular}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1>[t]
+  \small
+
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
+  \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 
+      & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
+  \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    
+      & \onslide<1->{\smath{X_1; a + X_2; a}}\\
+
+  & & & \onslide<2->{by Arden}\\
+
+  \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 
+      & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
+  \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    
+      & \only<2->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<4->{by Arden}\\
+
+  \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 
+      & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\
+  \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    
+      & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<5->{by substitution}\\
+
+  \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 
+      & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
+  \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    
+      & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<6->{by Arden}\\
+
+  \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 
+      & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+  \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    
+      & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<7->{by substitution}\\
+
+  \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 
+      & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+  \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    
+      & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
+          \cdot a\cdot a^\star}}\\
+  \end{tabular}
+  \end{center}
+
+  \only<8->{
+  \begin{textblock}{6}(2.5,4)
+  \begin{block}{}
+  \begin{minipage}{8cm}\raggedright
+  
+  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
+  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+
+  %\draw[help lines] (0,0) grid (3,2);
+
+  \node[state,initial]   (p_0)                  {$X_1$};
+  \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};
+
+  \path[->] (p_0) edge [bend left]   node        {a} (p_1)
+                  edge [loop above]   node       {b} ()
+            (p_1) edge [loop above]   node       {a} ()
+                  edge [bend left]   node        {b} (p_0);
+  \end{tikzpicture}
+
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
+
+  \only<1,2>{%
+  \begin{textblock}{3}(0.6,1.2)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<2>{%
+  \begin{textblock}{3}(0.6,3.6)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<4>{%
+  \begin{textblock}{3}(0.6,2.9)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<4>{%
+  \begin{textblock}{3}(0.6,5.3)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<5>{%
+  \begin{textblock}{3}(1.0,5.6)
+  \begin{tikzpicture}
+  \node at (0,0) (A) {};
+  \node at (0,1) (B) {};
+  \draw[<-, line width=2mm, red] (B) to  (A);
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<5,6>{%
+  \begin{textblock}{3}(0.6,7.7)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<6>{%
+  \begin{textblock}{3}(0.6,10.1)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<7>{%
+  \begin{textblock}{3}(1.0,10.3)
+  \begin{tikzpicture}
+  \node at (0,0) (A) {};
+  \node at (0,1) (B) {};
+  \draw[->, line width=2mm, red] (B) to  (A);
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE A Variant of Arden's Lemma}
+
+  {\bf Arden's Lemma:}\smallskip 
+
+  If \smath{[] \not\in A} then
+  \begin{center}
+  \smath{X = X; A + \text{something}}
+  \end{center}
+  has the (unique) solution
+  \begin{center}
+  \smath{X = \text{something} ; A^\star}
+  \end{center}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1-2,4->[t]
+  \small
+
+  \begin{center}
+  \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}
+  \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 
+      & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
+  \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    
+      & \onslide<1->{\smath{X_1; a + X_2; a}}\\
+
+  & & & \onslide<2->{by Arden}\\
+
+  \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 
+      & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\
+  \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    
+      & \only<2->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<4->{by Arden}\\
+
+  \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 
+      & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\
+  \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    
+      & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<5->{by substitution}\\
+
+  \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 
+      & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
+  \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    
+      & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<6->{by Arden}\\
+
+  \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 
+      & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+  \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    
+      & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\
+
+  & & & \onslide<7->{by substitution}\\
+
+  \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 
+      & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
+  \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    
+      & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 
+          \cdot a\cdot a^\star}}\\
+  \end{tabular}
+  \end{center}
+
+  \only<8->{
+  \begin{textblock}{6}(2.5,4)
+  \begin{block}{}
+  \begin{minipage}{8cm}\raggedright
+  
+  \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]
+  \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]
+
+  %\draw[help lines] (0,0) grid (3,2);
+
+  \node[state,initial]   (p_0)                  {$X_1$};
+  \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};
+
+  \path[->] (p_0) edge [bend left]   node        {a} (p_1)
+                  edge [loop above]   node       {b} ()
+            (p_1) edge [loop above]   node       {a} ()
+                  edge [bend left]   node        {b} (p_0);
+  \end{tikzpicture}
+
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
+
+  \only<1,2>{%
+  \begin{textblock}{3}(0.6,1.2)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<2>{%
+  \begin{textblock}{3}(0.6,3.6)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<4>{%
+  \begin{textblock}{3}(0.6,2.9)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<4>{%
+  \begin{textblock}{3}(0.6,5.3)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<5>{%
+  \begin{textblock}{3}(1.0,5.6)
+  \begin{tikzpicture}
+  \node at (0,0) (A) {};
+  \node at (0,1) (B) {};
+  \draw[<-, line width=2mm, red] (B) to  (A);
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<5,6>{%
+  \begin{textblock}{3}(0.6,7.7)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<6>{%
+  \begin{textblock}{3}(0.6,10.1)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]
+  {\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}}
+  \only<7>{%
+  \begin{textblock}{3}(1.0,10.3)
+  \begin{tikzpicture}
+  \node at (0,0) (A) {};
+  \node at (0,1) (B) {};
+  \draw[->, line width=2mm, red] (B) to  (A);
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE The Other Direction}
+
+  One has to prove
+
+  \begin{center}
+  \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}
+  \end{center}
+
+  by induction on \smath{r}. Not trivial, but after a bit 
+  of thinking, one can find a \alert{refined} relation:\bigskip
+
+  
+  \begin{center}
+  \mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c}
+  \begin{tikzpicture}[scale=1.1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1.1]
+  %Circle
+  \draw[thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 90,...,359}
+    \draw[very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}
+      \draw (\a: 0.65) node {\small$a_\l$};
+  \end{tikzpicture}
+  &
+  \begin{tikzpicture}[scale=1.1]
+  %Circle
+  \draw[red, thick] (0,0) circle (1.1);    
+  %Main rays
+  \foreach \a in {0, 45,...,359}
+     \draw[red, very thick] (0, 0) -- (\a:1.1);
+  \foreach \a / \l in {22.5/1.1, 67.5/1.2, 112.5/2.1, 157.5/2.2, 202.4/3.1, 247.5/3.2, 292.5/4.1, 337.5/4.2}
+      \draw (\a: 0.77) node {\textcolor{red}{\footnotesize$a_{\l}$}};
+  \end{tikzpicture}\\
+  \small\smath{U\!N\!IV} & 
+  \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &
+  \small\smath{U\!N\!IV /\!/ \alert{R}}
+  \end{tabular}}
+  \end{center}
+
+  \begin{textblock}{5}(9.8,2.6)
+  \begin{tikzpicture}
+  \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};
+  \end{tikzpicture}
+  \end{textblock}
+  
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\LARGE\begin{tabular}{c}Derivatives of RExps\end{tabular}}
+
+  \begin{itemize}
+  \item introduced by Brozowski~'64
+  \item produces a regular expression after a character has been parsed\\[-18mm]\mbox{}
+  \end{itemize}
+
+  \only<1->{%
+  \textcolor{blue}{%
+  \begin{center}
+  \begin{tabular}{@ {}lc@ {\hspace{3mm}}l@ {}}
+  der c $\varnothing$     & $\dn$ & $\varnothing$\\
+  der c []                & $\dn$ & $\varnothing$\\
+  der c d                 & $\dn$ & if c $=$ d then [] else $\varnothing$\\
+  der c ($r_1 + r_2$)     & $\dn$ & (der c $r_1$) $+$ (der c $r_2$)\\
+  der c ($r^\star$)       & $\dn$ & (der c $r$) $\cdot$ $r^\star$\\
+  der c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\
+                          &       & then (der c $r_1$) $\cdot$ $r_2$ $+$ (der c $r_2$)\\
+                          &       & else (der c $r_1$) $\cdot$ $r_2$\\
+  \end{tabular}
+  \end{center}}}
+
+  \only<2>{
+  \begin{textblock}{13}(1.5,5.7)
+  \begin{block}{}
+  \begin{quote}
+  \begin{minipage}{13cm}\raggedright
+  derivatives refine \smath{x \approx_{{\cal{L}}(r)} y}\bigskip
+  \begin{center}
+  \smath{\text{der}~x~r = \text{der}~y~r \Longrightarrow x \approx_{L(r)} y}
+  \end{center}\bigskip
+  \
+  \smath{\text{finite}(\text{ders}~A~r)}, but only modulo ACI
+
+  \begin{center}
+  \begin{tabular}{@ {\hspace{-10mm}}rcl}
+  \smath{(r_1 + r_2) + r_3} & \smath{\equiv} & \smath{r_1 + (r_2 + r_3)}\\
+  \smath{r_1 + r_2} &         \smath{\equiv} & \smath{r_2 + r_1}\\
+  \smath{r + r} &             \smath{\equiv} & \smath{r}\\
+  \end{tabular}
+  \end{center}
+  \end{minipage}
+  \end{quote}
+  \end{block}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<2>[t]
+  \frametitle{\LARGE\begin{tabular}{c}Derivatives of RExps\end{tabular}}
+
+ 
+  \only<2>{%
+  \textcolor{blue}{%
+  \begin{center}
+  \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+  pder c $\varnothing$     & $\dn$ & \alert{$\{\}$}\\
+  pder c []                & $\dn$ & \alert{$\{\}$}\\
+  pder c d                 & $\dn$ & if c $=$ d then $\{$[]$\}$ else $\{\}$\\
+  pder c ($r_1 + r_2$)     & $\dn$ & (pder c $r_1$) \alert{$\cup$} (der c $r_2$)\\
+  pder c ($r^\star$)       & $\dn$ & (pder c $r$) $\cdot$ $r^\star$\\
+  pder c ($r_1 \cdot r_2$) & $\dn$ & if nullable $r_1$\\
+                          &       & then (pder c $r_1$) $\cdot$ $r_2$ \alert{$\cup$} (pder c $r_2$)\\
+                          &       & else (pder c $r_1$) $\cdot$ $r_2$\\
+  \end{tabular}
+  \end{center}}}
+
+  \only<2>{
+  \begin{textblock}{6}(8.5,2.7)
+  \begin{block}{}
+  \begin{quote}
+  \begin{minipage}{6cm}\raggedright
+  \begin{itemize}
+  \item partial derivatives
+  \item by Antimirov~'95
+  \end{itemize}
+  \end{minipage}
+  \end{quote}
+  \end{block}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\LARGE Partial Derivatives}
+
+  \mbox{}\\[0mm]\mbox{}
+
+  \begin{itemize}
+
+  \item \alt<1>{\smath{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}}
+            {\smath{\underbrace{\text{pders $x$ $r$ \mbox{$=$} pders $y$ $r$}}_{R}}} 
+        refines \textcolor{blue}{$x$ $\approx_{{\cal L}(r)}$ $y$}\\[16mm]\pause
+  \item \smath{\text{finite} (U\!N\!IV /\!/ R)} \bigskip\pause
+  \item Therefore \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}. Qed.
+  \end{itemize}
+  
+  \only<2->{%
+  \begin{textblock}{5}(3.9,7.2)
+  \begin{tikzpicture}
+  \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};
+  \draw (2.2,0) node {Antimirov '95};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{\LARGE What Have We Achieved?}
+
+  \begin{itemize}
+  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
+  \medskip\pause
+  \item regular languages are closed under complementation; this is now easy
+  \begin{center}
+  \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}
+  \end{center}\pause\medskip
+  
+  \item non-regularity (\smath{a^nb^n})\medskip\pause\pause
+
+  \item take \alert{\bf any} language\\ build the language of substrings\\
+  \pause
+
+  then this language \alert{\bf is} regular\;\; (\smath{a^nb^n} $\Rightarrow$ \smath{a^\star{}b^\star})
+  
+  \end{itemize}
+
+\only<2>{
+\begin{textblock}{10}(4,14)
+\small
+\smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}
+\end{textblock}} 
+
+\only<4>{
+\begin{textblock}{5}(2,8.6)
+\begin{minipage}{8.8cm}
+\begin{block}{}
+\begin{minipage}{8.6cm}
+If there exists a sufficiently large set \smath{B} (for example infinitely large), 
+such that
+
+\begin{center}
+\smath{\forall x,y \in B.\; x \not= y \;\Rightarrow\; x \not\approx_{A} y}. 
+\end{center}  
+
+then \smath{A} is not regular.\hspace{1.3cm}\small(\smath{B \dn \bigcup_n a^n})
+\end{minipage}
+\end{block}
+\end{minipage}
+\end{textblock}
+}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
+
+  \begin{center}
+  \huge\bf\textcolor{gray}{in Nuprl}
+  \end{center}
+
+  \begin{itemize}
+  \item Constable, Jackson, Naumov, Uribe\medskip
+  \item \alert{18 months} for automata theory from Hopcroft \& Ullman chapters 1--11 (including Myhill-Nerode)
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
+
+  \begin{center}
+  \huge\bf\textcolor{gray}{in Coq}
+  \end{center}
+
+  \begin{itemize}
+  \item Filli\^atre, Briais, Braibant and others
+  \item multi-year effort; a number of results in automata theory, e.g.\medskip 
+    \begin{itemize}
+    \item Kleene's thm.~by Filli\^atre (\alert{``rather big''})
+    \item automata theory by Briais (5400 loc)
+    \item Braibant ATBR library, including Myhill-Nerode\\ ($>$7000 loc)
+    \item Mirkin's partial derivative automaton construction (10600 loc)
+    \end{itemize}
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}<1->[c]
+  \frametitle{}
+
+  \begin{center}
+  \includegraphics[scale=2.9]{numerals.jpg}
+  \end{center}
+  
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{\LARGE Conclusion}
+
+  \begin{itemize}
+  \item We have never seen a proof of Myhill-Nerode based on
+  regular expressions.\smallskip\pause
+
+  \item great source of examples (inductions)\smallskip\pause
+
+  \item no need to fight the theorem prover:\\ 
+  \begin{itemize}
+  \item first direction (790 loc)\\
+  \item second direction (400 / 390 loc)
+  \end{itemize}
+  
+  \item I am not saying automata are bad; just formal proofs about
+  them are shockingly difficult.
+  \end{itemize}
+
+  \only<4->{
+  \begin{textblock}{13.8}(1,4)
+  \begin{block}{}\mbox{}\hspace{3mm}
+  \begin{minipage}{11cm}\raggedright
+  \large 
+
+  {\bf Bold Claim: }\alert{(not proved!)}\medskip
+
+  {\bf 95\%} of regular language theory can be done without
+  automata!\medskip\\\ldots and this is much more tasteful ;o)
+
+  \end{minipage}
+  \end{block}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[b]
+  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Thank you very much!\\[5mm]Questions?}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+(*<*)
+end
+(*>*)
\ No newline at end of file




