(*<*)
theory Slides1
imports "~~/src/HOL/Library/LaTeXsugar"
begin

notation (latex output)
  set ("_") and
  Cons  ("_::/_" [66,65] 65) 

(*>*)


text_raw {*
  %\renewcommand{\slidecaption}{Cambridge, 9 November 2010}
  \renewcommand{\slidecaption}{Nijmegen, 25 August 2011}
  %%\renewcommand{\ULthickness}{2pt}
  \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=0pt, outer sep=0pt]
  \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}
  \frametitle{%
  \begin{tabular}{@ {}c@ {}}
  \Large A Formalisation of the\\[-4mm] 
  \Large Myhill-Nerode Theorem based on\\[-4mm] 
  \Large Regular Expressions\\[-4mm]
  \Large (Proof Pearl)\\[0mm] 
  \end{tabular}}
  
  \begin{center}
  \begin{tabular}{c@ {\hspace{15mm}}c}
  \includegraphics[scale=0.034]{chunhan.jpg} &
  \includegraphics[scale=0.034]{xingyuan.jpg}\\[-5mm]
  \end{tabular}
  \end{center}
 
  \begin{center}
  \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA
  University of Science and Technology in Nanjing
  \end{center}

  \begin{center}
  \small Christian Urban\\
  TU Munich
  \end{center}


  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{}

  \begin{textblock}{12.9}(1.5,3.2)
  \begin{block}{}
  \begin{minipage}{12.4cm}\raggedright
  \large I want to teach \alert{students} with\\ 
  theorem provers (especially inductions).
  \end{minipage}
  \end{block}
  \end{textblock}\pause

  \mbox{}\\[35mm]\mbox{}

  \begin{itemize}
  \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%
        \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip
  \item<3-> formal language theory \\
  \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman
  \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 Nuprl}
  \end{center}

  \begin{itemize}
  \item Constable, Jackson, Naumov, Uribe\medskip
  \item \alert{18 months} for automata theory, 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 ($>\!\!\!>$2000 loc)
    \item Mirkin's partial derivative automaton construction (10600 loc)
    \end{itemize}
  \end{itemize}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
  \mbox{}\\[-10mm]\mbox{}

  \begin{center}
  \huge\bf\textcolor{gray}{in HOL}
  \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 (C) to [red, very thick, bend left=45] (B);
  \draw (D) to [red, very thick, 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}{@ {}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 (Slind):\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->{A solution:\;\;\smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip}

  \only<7->{You have to \alert{\underline{rename}} states!}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[t]
  \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}
  \mbox{}\\[-10mm]\mbox{}

  \begin{center}
  \huge\bf\textcolor{gray}{in HOL}
  \end{center}

  \begin{itemize}
  \item Kozen's paper proof of Myhill-Nerode:\\ 
  \hspace{2cm}requires absence of \alert{inaccessible states}
  \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. Do we lose anything?\pause
  \begin{itemize}
  \item pumping lemma\pause
  \item closure under complementation\pause
  \item \only<6>{regular expression matching}%
       \only<7->{\sout{regular expression matching}}
  \item<8-> most textbooks are about automata
  \end{itemize}

  
  \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)}\medskip

  \item will help with closure properties of regular languages\bigskip\pause

  \item key is the equivalence relation:\smallskip
  \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.4,7.2)
  \begin{tikzpicture}
  \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]
  {@{text "\<lbrakk>x\<rbrakk>"}$_{\approx_{A}}$};
  \draw (0.9,-1.1) node {\begin{tabular}{l}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{final}_A\,X \dn \{[\!|x|\!]_{\approx_{A}}\;|\;x \in A\}}
  \smallskip
  \item we can prove: \smath{A = \bigcup \{X.\;\text{final}_A\,X\}}
  \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$};
  \draw[white] (0.9,0.5) node {$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)                  {$R_1$};
  \node[state,accepting] (p_1) [right of=q_0]   {$R_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{R_1} & \smath{\equiv} & \smath{R_1;b + R_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\
  & \smath{R_2} & \smath{\equiv} & \smath{R_1;a + R_2;a}\medskip\\
  \end{tabular}
  \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{R_1}} & \onslide<1->{\smath{=}} 
      & \onslide<1->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
  \onslide<1->{\smath{R_2}} & \onslide<1->{\smath{=}}    
      & \onslide<1->{\smath{R_1; a + R_2; a}}\\

  & & & \onslide<2->{by Arden}\\

  \onslide<2->{\smath{R_1}} & \onslide<2->{\smath{=}} 
      & \onslide<2->{\smath{R_1; b + R_2; b + \lambda;[]}}\\
  \onslide<2->{\smath{R_2}} & \onslide<2->{\smath{=}}    
      & \only<2->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<4->{by Arden}\\

  \onslide<4->{\smath{R_1}} & \onslide<4->{\smath{=}} 
      & \onslide<4->{\smath{R_2; b \cdot b^\star+ \lambda;b^\star}}\\
  \onslide<4->{\smath{R_2}} & \onslide<4->{\smath{=}}    
      & \onslide<4->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<5->{by substitution}\\

  \onslide<5->{\smath{R_1}} & \onslide<5->{\smath{=}} 
      & \onslide<5->{\smath{R_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\
  \onslide<5->{\smath{R_2}} & \onslide<5->{\smath{=}}    
      & \onslide<5->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<6->{by Arden}\\

  \onslide<6->{\smath{R_1}} & \onslide<6->{\smath{=}} 
      & \onslide<6->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
  \onslide<6->{\smath{R_2}} & \onslide<6->{\smath{=}}    
      & \onslide<6->{\smath{R_1; a\cdot a^\star}}\\

  & & & \onslide<7->{by substitution}\\

  \onslide<7->{\smath{R_1}} & \onslide<7->{\smath{=}} 
      & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\
  \onslide<7->{\smath{R_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)                  {$R_1$};
  \node[state,accepting] (p_1) [right of=q_0]   {$R_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}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}


text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE 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}

  
  

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\LARGE What Have We Achieved?}

  \begin{itemize}
  \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}
  \bigskip\pause
  \item regular languages are closed under complementation; this is easy
  \begin{center}
  \smath{U\!N\!IV /\!/ \approx_A \;\;=\;\; U\!N\!IV /\!/ \approx_{\overline{A}}}
  \end{center}\pause\bigskip
  
  \item non-regularity (\smath{a^nb^n})

  \begin{quote}
  \begin{minipage}{8.8cm}
  \begin{block}{}
  \begin{minipage}{8.6cm}
  If there exists a sufficiently large set \smath{B} (for example infinite), 
  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.
  \end{minipage}
  \end{block}
  \end{minipage}\medskip\pause

  \small(\smath{A \dn \bigcup_i a^i})
  \end{quote}

  \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}
  }

  

  \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)\pause
  \end{itemize}\smallskip

  \item I have \alert{\bf not} yet used it for teaching of undergraduates.\pause

  \end{itemize}

  \only<5->{
  \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 this is much more tasteful. ;o)

  \end{minipage}
  \end{block}
  \end{textblock}}

  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

text_raw {*
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
  \mode<presentation>{
  \begin{frame}[c]
  \frametitle{\mbox{}\\[2cm]\textcolor{red}{Questions?}}



  \end{frame}}
  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
*}

(*<*)
end
(*>*)