1 (*<*)

     2 theory Slides5

     3 imports "~~/src/HOL/Library/LaTeXsugar"

     4 begin

     5 

     6 notation (latex output)

     7   set ("_") and

     8   Cons  ("_::/_" [66,65] 65) 

     9 

    10 (*>*)

    11 

    12 

    13 text_raw {*

    14   \renewcommand{\slidecaption}{London, 29 August 2012}

    15   \newcommand{\bl}[1]{\textcolor{blue}{#1}}                        

    16   \newcommand{\sout}[1]{\tikz[baseline=(X.base), inner sep=-0.1pt, outer sep=0pt]

    17   \node [cross out,red, ultra thick, draw] (X) {\textcolor{black}{#1}};}

    18   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    19   \mode<presentation>{

    20   \begin{frame}

    21   \frametitle{%

    22   \begin{tabular}{@ {}c@ {}}

    23   \\[-3mm]

    24   \LARGE The Myhill-Nerode Theorem\\[-3mm] 

    25   \LARGE in a Theorem Prover\\[0mm] 

    26   \end{tabular}}

    27   

    28   \begin{center}

    29    Christian Urban\\

    30   \small King's College London

    31   \end{center}\bigskip

    32  

    33   \begin{center}

    34   \small joint work with Chunhan Wu and Xingyuan Zhang from the PLA

    35   University of Science and Technology in Nanjing

    36   \end{center}

    37 

    38   \only<2->{

    39   \begin{textblock}{6}(9,5.3)

    40   \alert{\bf Isabelle/HOL}

    41   \end{textblock}}

    42 

    43   \end{frame}}

    44   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    45 *}

    46 

    47 text_raw {*

    48   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    49   \mode<presentation>{

    50   \begin{frame}<1->[c]

    51   \frametitle{}

    52 

    53   \mbox{}\\[2mm]

    54   \begin{itemize}

    55   \item my background is in 

    56   \begin{itemize}

    57   \item \normalsize programming languages and theorem provers

    58   \item \normalsize develop Nominal Isabelle

    59   \end{itemize}\bigskip\bigskip\bigskip\bigskip\bigskip  

    60 

    61   \item<1->to formalise and mechanically check proofs from 

    62   programming language research, TCS \textcolor{gray}{and OS}\bigskip

    63 

    64   \item<2->we found out that the variable convention can lead to

    65   faulty proofs\ldots 

    66   \end{itemize}

    67   

    68   \onslide<2->{

    69   \begin{center}

    70   \begin{block}{}

    71   \color{gray}

    72   \footnotesize

    73   {\bf\mbox{}\hspace{-1.5mm}Variable Convention:}\\[0mm] 

    74   If $M_1,\ldots,M_n$ occur in a certain mathematical context

    75   (e.g. definition, proof), then in these terms all bound variables 

    76   are chosen to be different from the free variables.\hfill Henk Barendregt

    77   \end{block}

    78   \end{center}}

    79 

    80 

    81   \only<1->{

    82   \begin{textblock}{6}(10.9,3.5)

    83   \includegraphics[scale=0.23]{isabelle1.png}

    84   \end{textblock}}

    85   

    86 

    87 

    88   \end{frame}}

    89   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

    90 *}

    91 

    92 

    93 

    94 

    95 text_raw {*

    96   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

    97   \mode<presentation>{

    98   \begin{frame}[c]

    99   \frametitle{}

   100 

   101   \begin{tabular}{c@ {\hspace{2mm}}c}

   102   \\[6mm]

   103   \begin{tabular}{c}

   104   \includegraphics[scale=0.11]{harper.jpg}\\[-2mm]

   105   {\footnotesize Bob Harper}\\[-2.5mm]

   106   {\footnotesize (CMU)}

   107   \end{tabular}

   108   \begin{tabular}{c}

   109   \includegraphics[scale=0.37]{pfenning.jpg}\\[-2mm]

   110   {\footnotesize Frank Pfenning}\\[-2.5mm]

   111   {\footnotesize (CMU)}

   112   \end{tabular} &

   113 

   114   \begin{tabular}{p{6cm}}

   115   \raggedright

   116   \color{gray}{published a proof on LF in\\ {\bf ACM Transactions on Computational Logic}, 2005,

   117   $\sim$31pp}

   118   \end{tabular}\\

   119 

   120   \pause

   121   \\[0mm]

   122   

   123   \begin{tabular}{c}

   124   \includegraphics[scale=0.36]{appel.jpg}\\[-2mm] 

   125   {\footnotesize Andrew Appel}\\[-2.5mm]

   126   {\footnotesize (Princeton)}

   127   \end{tabular} &

   128 

   129   \begin{tabular}{p{6cm}}

   130   \raggedright

   131   \color{gray}{relied on their proof in a\\ {\bf security} critical application\\ (proof-carrying code)}

   132   \end{tabular}

   133   \end{tabular}

   134 

   135   

   136 

   137   \end{frame}}

   138   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   139 *}

   140 

   141 

   142 

   143 text {*

   144   \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]

   145   \tikzstyle{node1}=[rectangle, minimum size=10mm, rounded corners=3mm, very thick, 

   146                      draw=black!50, top color=white, bottom color=black!20]

   147   \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 

   148                      draw=red!70, top color=white, bottom color=red!50!black!20]

   149   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   150   \mode<presentation>{

   151   \begin{frame}<2->[squeeze]

   152   \frametitle{} 

   153   

   154   \begin{columns}

   155   

   156   \begin{column}{0.8\textwidth}

   157   \begin{textblock}{0}(1,2)

   158 

   159   \begin{tikzpicture}

   160   \matrix[ampersand replacement=\&,column sep=7mm, row sep=5mm]

   161   { \&[-10mm] 

   162     \node (def1)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}}; \&

   163     \node (proof1) [node1] {\large Proof}; \&

   164     \node (alg1)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}}; \\

   165     

   166     \onslide<4->{\node {\begin{tabular}{c}\small 1st\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   167     \onslide<4->{\node (def2)   [node2] {\large Spec$^\text{+ex}$};} \&

   168     \onslide<4->{\node (proof2) [node1] {\large Proof};} \&

   169     \onslide<4->{\node (alg2)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   170      

   171     \onslide<5->{\node {\begin{tabular}{c}\small 2nd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   172     \onslide<5->{\node (def3)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   173     \onslide<5->{\node (proof3) [node1] {\large Proof};} \&

   174     \onslide<5->{\node (alg3)   [node2] {\large Alg$^\text{-ex}$};} \\

   175 

   176     \onslide<6->{\node {\begin{tabular}{c}\small 3rd\\[-2.5mm] \footnotesize solution\end{tabular}};} \&

   177     \onslide<6->{\node (def4)   [node1] {\large\hspace{1mm}Spec\hspace{1mm}\mbox{}};} \&

   178     \onslide<6->{\node (proof4) [node2] {\large\hspace{1mm}Proof\hspace{1mm}};} \&

   179     \onslide<6->{\node (alg4)   [node1] {\large\hspace{1mm}Alg\hspace{1mm}\mbox{}};} \\

   180   };

   181 

   182   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   183   \draw[->,black!50,line width=2mm] (proof1) -- (alg1);

   184   

   185   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (def2);}

   186   \onslide<4->{\draw[->,black!50,line width=2mm] (proof2) -- (alg2);}

   187 

   188   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (def3);}

   189   \onslide<5->{\draw[->,black!50,line width=2mm] (proof3) -- (alg3);}

   190   

   191   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (def4);}

   192   \onslide<6->{\draw[->,black!50,line width=2mm] (proof4) -- (alg4);}

   193 

   194   \onslide<3->{\draw[white,line width=1mm] (1.1,3.2) -- (0.9,2.85) -- (1.1,2.35) -- (0.9,2.0);} 

   195   \end{tikzpicture}

   196 

   197   \end{textblock}

   198   \end{column}

   199   \end{columns}

   200 

   201 

   202   \begin{textblock}{3}(12,3.6)

   203   \onslide<4->{

   204   \begin{tikzpicture}

   205   \node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{2h};

   206   \end{tikzpicture}}

   207   \end{textblock}

   208 

   209   \end{frame}}

   210   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   211 

   212 *}

   213 

   214 

   215 text_raw {*

   216   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   217   \mode<presentation>{

   218   \begin{frame}[c]

   219   \frametitle{}

   220 

   221   \begin{itemize}

   222   \item I also found fixable errors in my Ph.D.-thesis about cut-elimination

   223   (examined by Henk Barendregt and Andy Pitts)\bigskip

   224   \item found flaws in a proof about a classic OS scheduling algorithm

   225   --- helped us to implement\\ it correctly and ef$\!$ficiently\\ 

   226   {\small\textcolor{gray}{(the existing literature ``proved'' 

   227   correct an incorrect algorithm; used in the Mars Pathfinder mission)}}

   228   \end{itemize}\bigskip\bigskip\pause

   229 

   230 

   231   {\bf Conclusion:}\smallskip

   232 

   233   Pencil-and-paper proofs in TCS are not foolproof, 

   234   not even expertproof.

   235 

   236   \end{frame}}

   237   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   238 *}

   239 

   240 

   241 text_raw {*

   242   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   243   \mode<presentation>{

   244   \begin{frame}[t]

   245 

   246   \small Scott Aaronson (Berkeley/MIT):\\[-7mm]\mbox{}

   247   \begin{center}

   248   \begin{block}{}

   249   \color{gray}

   250   \small

   251   ``I still remember having to grade hundreds of exams where the

   252   students started out by assuming what had to be proved, or filled

   253   page after page with gibberish in the hope that, somewhere in the

   254   mess, they might accidentally have said something

   255   correct. \ldots{}innumerable examples of ``parrot proofs'' ---

   256   NP-completeness reductions done in the wrong direction, arguments

   257   that look more like LSD trips than coherent chains of logic \ldots{}''

   258   \end{block}

   259   \end{center}\pause

   260 

   261   \begin{tabular}{@ {}c@ {}}

   262   Tobias Nipkow calls this the ``London Underground Phenomenon'':

   263   \end{tabular}

   264 

   265   \begin{center}

   266   \begin{tabular}{ccc}

   267   students & \;\;\raisebox{-8mm}{\includegraphics[scale=0.16]{gap.jpg}}\;\; & proofs

   268   \end{tabular}

   269   \end{center}

   270 

   271   \end{frame}}

   272   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   273 *}

   274 

   275 text_raw {*

   276   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   277   \mode<presentation>{

   278   \begin{frame}[c]

   279   \frametitle{}

   280 

   281   \begin{textblock}{12.9}(1.5,2.0)

   282   \begin{block}{}

   283   \begin{minipage}{12.4cm}\raggedright

   284   \large {\bf Motivation:}\\[2mm]I want to teach \alert{students} with

   285   theorem\\ provers (especially for inductions).

   286   \end{minipage}

   287   \end{block}

   288   \end{textblock}\pause

   289 

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

   291 

   292   \begin{itemize}

   293   \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%

   294         \only<3->{\sout{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}\medskip

   295   \item<3-> formal language theory \\

   296   \mbox{}\;\;@{text "\<Rightarrow>"} nice textbooks: Kozen, Hopcroft \& Ullman\ldots

   297   \end{itemize}

   298 

   299   \end{frame}}

   300   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   301 

   302 *}

   303 

   304 

   305 text_raw {*

   306   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   307   \mode<presentation>{

   308   \begin{frame}<1->[t]

   309   \frametitle{Regular Expressions}

   310 

   311   \begin{textblock}{6}(2,4)

   312   \begin{tabular}{@ {}rrl}

   313   \bl{r} & \bl{$::=$}  & \bl{$\varnothing$}\\

   314          & \bl{$\mid$} & \bl{[]}\\

   315          & \bl{$\mid$} & \bl{c}\\

   316          & \bl{$\mid$} & \bl{r$_1$ $\cdot$ r$_2$}\\

   317          & \bl{$\mid$} & \bl{r$_1$ + r$_2$}\\

   318          & \bl{$\mid$} & \bl{r$^*$}\\

   319   \end{tabular}

   320   \end{textblock}

   321 

   322   \begin{textblock}{6}(8,3.5)

   323   \includegraphics[scale=0.35]{Screen1.png}

   324   \end{textblock}

   325 

   326   \begin{textblock}{6}(10.2,2.8)

   327   \footnotesize Isabelle:

   328   \end{textblock}

   329 

   330   \begin{textblock}{6}(7,12)

   331   \footnotesize\textcolor{gray}{students have seen them and can be motivated about them}

   332   \end{textblock}

   333   

   334   \end{frame}}

   335   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   336 *}

   337 

   338 text_raw {*

   339   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   340   \mode<presentation>{

   341   \begin{frame}<1->[t]

   342 

   343   \mbox{}\\[-2mm]

   344 

   345   \small

   346   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}ll@ {}}

   347   \bl{nullable ($\varnothing$)}            & \bl{$=$} & \bl{false} &\\

   348   \bl{nullable ([])}           & \bl{$=$} & \bl{true}  &\\

   349   \bl{nullable (c)}           & \bl{$=$} & \bl{false} &\\

   350   \bl{nullable (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\vee$ (nullable r$_2$)} & \\ 

   351   \bl{nullable (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{(nullable r$_1$) $\wedge$ (nullable r$_2$)} & \\

   352   \bl{nullable (r$^*$)}          & \bl{$=$} & \bl{true} & \\

   353   \end{tabular}\medskip\pause

   354 

   355   \begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {\hspace{-10mm}}l@ {}}

   356   \bl{der c ($\varnothing$)}            & \bl{$=$} & \bl{$\varnothing$} & \\

   357   \bl{der c ([])}           & \bl{$=$} & \bl{$\varnothing$} & \\

   358   \bl{der c (d)}           & \bl{$=$} & \bl{if c $=$ d then [] else $\varnothing$} & \\

   359   \bl{der c (r$_1$ + r$_2$)} & \bl{$=$} & \bl{(der c r$_1$) + (der c r$_2$)} & \\

   360   \bl{der c (r$_1$ $\cdot$ r$_2$)} & \bl{$=$} & \bl{((der c r$_1$) $\cdot$ r$_2$) + } & \\

   361        &          & \bl{\hspace{3mm}(if nullable r$_1$ then der c r$_2$ else $\varnothing$)}\\

   362   \bl{der c (r$^*$)}          & \bl{$=$} & \bl{(der c r) $\cdot$ (r$^*$)} &\smallskip\\\pause

   363 

   364   \bl{derivative [] r}     & \bl{$=$} & \bl{r} & \\

   365   \bl{derivative (c::s) r} & \bl{$=$} & \bl{derivative s (der c r)} & \\

   366   \end{tabular}\medskip

   367 

   368   \bl{matches r s $=$ nullable (derivative s r)}

   369   

   370   \end{frame}}

   371   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   372 *}

   373 

   374 text_raw {*

   375   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   376   \mode<presentation>{

   377   \begin{frame}[c]

   378   \frametitle{\LARGE Regular Expression Matching\\[-2mm] in Education}

   379 

   380   \begin{itemize}

   381   \item Harper in JFP'99: ``Functional Pearl: Proof- Directed Debugging''\medskip

   382   \item Yi in JFP'06: ``Educational Pearl: `Proof-Directed Debugging' revisited 

   383   for a first-order version''\medskip\bigskip\bigskip\pause

   384   \item Owens et al in JFP'09: ``Regular-expression derivatives re-examined''

   385   \bigskip

   386 

   387   \begin{quote}\small

   388   ``Unfortunately, regular expression derivatives have been lost in the 

   389   sands of time, and few computer scientists are aware of them.''

   390   \end{quote}

   391   \end{itemize}

   392   

   393 

   394   \end{frame}}

   395   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   396 

   397 *}

   398 

   399 text_raw {*

   400   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   401   \mode<presentation>{

   402   \begin{frame}[t]

   403   \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

   404   \mbox{}\\[-15mm]\mbox{}

   405 

   406   \begin{center}

   407   \huge\bf\textcolor{gray}{in Theorem Provers}\\

   408   \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

   409   \end{center}

   410 

   411   \begin{itemize}

   412   \item automata @{text "\<Rightarrow>"} graphs, matrices, functions

   413   \item<2-> combining automata / graphs

   414 

   415   \onslide<2->{

   416   \begin{center}

   417   \begin{tabular}{ccc}

   418   \begin{tikzpicture}[scale=1]

   419   %\draw[step=2mm] (-1,-1) grid (1,1);

   420   

   421   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

   422   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

   423 

   424   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   425   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   426   

   427   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   428   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   429 

   430   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   431   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   432   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   433 

   434   \draw (-0.6,0.0) node {\small$A_1$};

   435   \draw ( 0.6,0.0) node {\small$A_2$};

   436   \end{tikzpicture}}

   437 

   438   & 

   439 

   440   \onslide<3->{\raisebox{1.1mm}{\bf\Large$\;\Rightarrow\,$}}

   441 

   442   &

   443 

   444   \onslide<3->{\begin{tikzpicture}[scale=1]

   445   %\draw[step=2mm] (-1,-1) grid (1,1);

   446   

   447   \draw[rounded corners=1mm, very thick] (-1.0,-0.3) rectangle (-0.2,0.3);

   448   \draw[rounded corners=1mm, very thick] ( 0.2,-0.3) rectangle ( 1.0,0.3);

   449 

   450   \node (A) at (-1.0,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   451   \node (B) at ( 0.2,0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   452   

   453   \node (C) at (-0.2, 0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   454   \node (D) at (-0.2,-0.13) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   455 

   456   \node (E) at (1.0, 0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   457   \node (F) at (1.0,-0.0) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   458   \node (G) at (1.0,-0.2) [circle, very thick, draw, fill=white, inner sep=0.4mm] {};

   459   

   460   \draw [very thick, red] (C) to [bend left=45] (B);

   461   \draw [very thick, red] (D) to [bend right=45] (B);

   462 

   463   \draw (-0.6,0.0) node {\small$A_1$};

   464   \draw ( 0.6,0.0) node {\small$A_2$};

   465   \end{tikzpicture}}

   466 

   467   \end{tabular}

   468   \end{center}\medskip

   469 

   470   \only<4-5>{

   471   \begin{tabular}{@ {\hspace{-5mm}}l@ {}}

   472   disjoint union:\\[2mm]

   473   \smath{A_1\uplus A_2 \dn \{(1, x)\,|\, x \in A_1\} \,\cup\, \{(2, y)\,|\, y \in A_2\}}

   474   \end{tabular}}

   475   \end{itemize}

   476 

   477   \only<5>{

   478   \begin{textblock}{13.9}(0.7,7.7)

   479   \begin{block}{}

   480   \medskip

   481   \begin{minipage}{14cm}\raggedright

   482   Problems with definition for regularity:\bigskip\\

   483   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}\bigskip

   484   \end{minipage}

   485   \end{block}

   486   \end{textblock}}

   487   \medskip

   488 

   489   \only<6->{\underline{A solution}:\;\;use \smath{\text{nat}}s \;@{text "\<Rightarrow>"}\; state nodes\medskip}

   490 

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

   492 

   493   \end{frame}}

   494   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   495 *}

   496 

   497 text_raw {*

   498   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   499   \mode<presentation>{

   500   \begin{frame}[t]

   501   \frametitle{\normalsize Formal language theory\ldots\hfill\mbox{}}

   502   \mbox{}\\[-15mm]\mbox{}

   503 

   504   \begin{center}

   505   \huge\bf\textcolor{gray}{in Theorem Provers}\\

   506   \footnotesize\textcolor{gray}{e.g.~Isabelle, Coq, HOL4, \ldots}

   507   \end{center}

   508 

   509   \begin{itemize}

   510   \item Kozen's paper-proof of Myhill-Nerode:\\ 

   511   requires absence of \alert{inaccessible states}

   512   \item complementation of automata only works for \alert{complete} automata

   513   (need sink states)\medskip

   514   \end{itemize}\bigskip\bigskip

   515 

   516   \begin{center}

   517   \smath{\;\text{is\_regular}(A) \dn \exists M.\;\text{is\_dfa}(M) \wedge {\cal L} (M) = A}

   518   \end{center}

   519 

   520 

   521   \end{frame}}

   522   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   523 *}

   524 

   525 text_raw {*

   526   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   527   \mode<presentation>{

   528   \begin{frame}[t]

   529   \frametitle{}

   530   \mbox{}\\[25mm]\mbox{}

   531 

   532   \begin{textblock}{13.9}(0.7,1.2)

   533   \begin{block}{}

   534   \begin{minipage}{13.4cm}\raggedright

   535   {\bf Definition:}\smallskip\\

   536   

   537   A language \smath{A} is \alert{regular}, provided there exists a\\ 

   538   \alert{regular expression} that matches all strings of \smath{A}.

   539   \end{minipage}

   540   \end{block}

   541   \end{textblock}\pause

   542   

   543   {\noindent\large\bf\alert{\ldots{}and forget about automata}}\bigskip\bigskip\pause

   544 

   545   Infrastructure for free. But do we lose anything?\medskip\pause

   546 

   547   \begin{minipage}{1.1\textwidth}

   548   \begin{itemize}

   549   \item pumping lemma\pause

   550   \item closure under complementation\pause

   551   \item \only<6>{regular expression matching}%

   552        \only<7->{\sout{regular expression matching}

   553   {\footnotesize(@{text "\<Rightarrow>"}Brzozowski'64, Owens et al '09)}}

   554   \item<8-> most textbooks are about automata

   555   \end{itemize}

   556   \end{minipage}

   557 

   558   

   559   \end{frame}}

   560   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   561 

   562 *}

   563 

   564 

   565 text_raw {*

   566   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   567   \mode<presentation>{

   568   \begin{frame}[c]

   569   \frametitle{\LARGE The Myhill-Nerode Theorem}

   570 

   571   \begin{itemize}

   572   \item provides necessary and suf\!ficient conditions\\ for a language 

   573   being regular\\ \textcolor{gray}{(pumping lemma only necessary)}\bigskip

   574 

   575   \item key is the equivalence relation:\medskip

   576   \begin{center}

   577   \smath{x \approx_{A} y \,\dn\, \forall z.\; x @ z \in A \Leftrightarrow y @ z \in A}

   578   \end{center}

   579   \end{itemize}

   580 

   581  

   582   \end{frame}}

   583   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   584 

   585 *}

   586 

   587 text_raw {*

   588   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   589   \mode<presentation>{

   590   \begin{frame}[c]

   591   \frametitle{\LARGE The Myhill-Nerode Theorem}

   592 

   593   \begin{center}

   594   \only<1>{%

   595   \begin{tikzpicture}[scale=3]

   596   \draw[very thick] (0.5,0.5) circle (.6cm);

   597   \end{tikzpicture}}%

   598   \only<2->{%

   599   \begin{tikzpicture}[scale=3]

   600   \draw[very thick] (0.5,0.5) circle (.6cm);

   601   \clip[draw] (0.5,0.5) circle (.6cm);

   602   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

   603   \end{tikzpicture}}

   604   \end{center}

   605   

   606   \begin{itemize}

   607   \item \smath{\text{finite}\, (U\!N\!IV /\!/ \approx_A) \;\Leftrightarrow\; A\; \text{is regular}}

   608   \end{itemize}

   609 

   610   \begin{textblock}{5}(2.1,5.3)

   611   \begin{tikzpicture}

   612   \node at (0,0) [single arrow, fill=red,text=white, minimum height=2cm]

   613   {$U\!N\!IV$};

   614   \draw (-0.3,-1.1) node {\begin{tabular}{l}set of all\\[-1mm] strings\end{tabular}};

   615   \end{tikzpicture}

   616   \end{textblock}

   617 

   618   \only<2->{%

   619   \begin{textblock}{5}(9.1,7.2)

   620   \begin{tikzpicture}

   621   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]

   622   {@{text "\<lbrakk>s\<rbrakk>"}$_{\approx_{A}}$};

   623   \draw (0.9,-1.1) node {\begin{tabular}{l}an equivalence class\end{tabular}};

   624   \end{tikzpicture}

   625   \end{textblock}}

   626 

   627   \only<3->{

   628   \begin{textblock}{11.9}(1.7,3)

   629   \begin{block}{}

   630   \begin{minipage}{11.4cm}\raggedright

   631   Two directions:\medskip\\

   632   \begin{tabular}{@ {}ll}

   633   1.)\;finite $\Rightarrow$ regular\\

   634   \;\;\;\smath{\text{finite}\,(U\!N\!IV /\!/ \approx_A) \Rightarrow \exists r.\;A = {\cal L}(r)}\\[3mm]

   635   2.)\;regular $\Rightarrow$ finite\\

   636   \;\;\;\smath{\text{finite}\, (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}

   637   \end{tabular}

   638 

   639   \end{minipage}

   640   \end{block}

   641   \end{textblock}}

   642 

   643   \end{frame}}

   644   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   645 

   646 *}

   647 

   648 

   649 text_raw {*

   650   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   651   \mode<presentation>{

   652   \begin{frame}[c]

   653   \frametitle{\LARGE Initial and Final {\sout{\textcolor{gray}{States}}}}

   654 

   655   \begin{textblock}{8}(10, 2)

   656   \textcolor{black}{Equivalence Classes}

   657   \end{textblock}

   658 

   659 

   660   \begin{center}

   661   \begin{tikzpicture}[scale=3]

   662   \draw[very thick] (0.5,0.5) circle (.6cm);

   663   \clip[draw] (0.5,0.5) circle (.6cm);

   664   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

   665   \only<2->{\draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);}

   666   \only<3->{\draw[red, fill] (0.2, 0.2) rectangle (0.4, 0.4);

   667   \draw[red, fill] (0.4, 0.8) rectangle (0.6, 1.0);

   668   \draw[red, fill] (0.6, 0.0) rectangle (0.8, 0.2);

   669   \draw[red, fill] (0.8, 0.4) rectangle (1.0, 0.6);}

   670   \end{tikzpicture}

   671   \end{center}

   672 

   673   \begin{itemize}

   674   \item \smath{\text{finals}\,A\,\dn \{[\!|s|\!]_{\approx_{A}}\;|\;s \in A\}}

   675   \smallskip

   676   \item we can prove: \smath{A = \bigcup \text{finals}\,A}

   677   \end{itemize}

   678 

   679   \only<2->{%

   680   \begin{textblock}{5}(2.1,4.6)

   681   \begin{tikzpicture}

   682   \node at (0,0) [single arrow, fill=blue,text=white, minimum height=2cm]

   683   {$[] \in X$};

   684   \end{tikzpicture}

   685   \end{textblock}}

   686 

   687   \only<3->{%

   688   \begin{textblock}{5}(10,7.4)

   689   \begin{tikzpicture}

   690   \node at (0,0) [shape border rotate=180,single arrow, fill=red,text=white, minimum height=2cm]

   691   {a final};

   692   \end{tikzpicture}

   693   \end{textblock}}

   694 

   695   \end{frame}}

   696   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   697 *}

   698 

   699 

   700 text_raw {*

   701   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   702   \mode<presentation>{

   703   \begin{frame}<-1>[c]

   704   \frametitle{\begin{tabular}{@ {}l}\LARGE% 

   705   Transitions between Eq-Classes\end{tabular}}

   706 

   707   \begin{center}

   708   \begin{tikzpicture}[scale=3]

   709   \draw[very thick] (0.5,0.5) circle (.6cm);

   710   \clip[draw] (0.5,0.5) circle (.6cm);

   711   \draw[step=2mm, very thick] (-1.4,-1.4) grid (1.4,1.4);

   712   \draw[blue, fill] (0.0, 0.6) rectangle (0.2, 0.8);

   713   \draw[blue, fill] (0.8, 0.4) rectangle (1.0, 0.6);

   714   \draw[white] (0.1,0.7) node (X) {$X$};

   715   \draw[white] (0.9,0.5) node (Y) {$Y$};

   716   \draw[blue, ->, line width = 2mm, bend left=45] (X) -- (Y);

   717   \node [inner sep=1pt,label=above:\textcolor{blue}{$c$}] at ($ (X)!.5!(Y) $) {};

   718   \end{tikzpicture}

   719   \end{center}

   720 

   721   \begin{center}

   722   \smath{X \stackrel{c}{\longrightarrow} Y \;\dn\; X ; c \subseteq Y}

   723   \end{center}

   724 

   725   \onslide<8>{

   726   \begin{tabular}{c}

   727   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]

   728   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   729   \node[state,initial] (q_0) {$R_1$};

   730   \end{tikzpicture}

   731   \end{tabular}}

   732 

   733   \end{frame}}

   734   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   735 *}

   736 

   737 

   738 text_raw {*

   739   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   740   \mode<presentation>{

   741   \begin{frame}[c]

   742   \frametitle{\LARGE Systems of Equations}

   743 

   744   Inspired by a method of Brzozowski\;'64:\bigskip\bigskip

   745 

   746   \begin{center}

   747   \begin{tabular}{@ {\hspace{-20mm}}c}

   748   \\[-13mm]

   749   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick]

   750   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   751 

   752   %\draw[help lines] (0,0) grid (3,2);

   753 

   754   \node[state,initial]   (p_0)                  {$X_1$};

   755   \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};

   756 

   757   \path[->] (p_0) edge [bend left]   node        {a} (p_1)

   758                   edge [loop above]   node       {b} ()

   759             (p_1) edge [loop above]   node       {a} ()

   760                   edge [bend left]   node        {b} (p_0);

   761   \end{tikzpicture}\\

   762   \\[-13mm]

   763   \end{tabular}

   764   \end{center}

   765 

   766   \begin{center}

   767   \begin{tabular}{@ {\hspace{-6mm}}ll@ {\hspace{1mm}}c@ {\hspace{1mm}}l}

   768   & \smath{X_1} & \smath{=} & \smath{X_1;b + X_2;b \onslide<2->{\alert<2>{+ \lambda;[]}}}\\

   769   & \smath{X_2} & \smath{=} & \smath{X_1;a + X_2;a}\medskip\\

   770   \end{tabular}

   771   \end{center}

   772 

   773   \end{frame}}

   774   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   775 *}

   776 

   777 text_raw {*

   778   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   779   \mode<presentation>{

   780   \begin{frame}<1>[t]

   781   \small

   782 

   783   \begin{center}

   784   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}

   785   \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 

   786       & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   787   \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    

   788       & \onslide<1->{\smath{X_1; a + X_2; a}}\\

   789 

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

   791 

   792   \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 

   793       & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   794   \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    

   795       & \only<2->{\smath{X_1; a\cdot a^\star}}\\

   796 

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

   798 

   799   \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 

   800       & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\

   801   \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    

   802       & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\

   803 

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

   805 

   806   \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 

   807       & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\

   808   \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    

   809       & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\

   810 

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

   812 

   813   \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 

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

   815   \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    

   816       & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\

   817 

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

   819 

   820   \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 

   821       & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\

   822   \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    

   823       & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 

   824           \cdot a\cdot a^\star}}\\

   825   \end{tabular}

   826   \end{center}

   827 

   828   \only<8->{

   829   \begin{textblock}{6}(2.5,4)

   830   \begin{block}{}

   831   \begin{minipage}{8cm}\raggedright

   832   

   833   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]

   834   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   835 

   836   %\draw[help lines] (0,0) grid (3,2);

   837 

   838   \node[state,initial]   (p_0)                  {$X_1$};

   839   \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};

   840 

   841   \path[->] (p_0) edge [bend left]   node        {a} (p_1)

   842                   edge [loop above]   node       {b} ()

   843             (p_1) edge [loop above]   node       {a} ()

   844                   edge [bend left]   node        {b} (p_0);

   845   \end{tikzpicture}

   846 

   847   \end{minipage}

   848   \end{block}

   849   \end{textblock}}

   850 

   851   \only<1,2>{%

   852   \begin{textblock}{3}(0.6,1.2)

   853   \begin{tikzpicture}

   854   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   855   {\textcolor{red}{a}};

   856   \end{tikzpicture}

   857   \end{textblock}}

   858   \only<2>{%

   859   \begin{textblock}{3}(0.6,3.6)

   860   \begin{tikzpicture}

   861   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   862   {\textcolor{red}{a}};

   863   \end{tikzpicture}

   864   \end{textblock}}

   865   \only<4>{%

   866   \begin{textblock}{3}(0.6,2.9)

   867   \begin{tikzpicture}

   868   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   869   {\textcolor{red}{a}};

   870   \end{tikzpicture}

   871   \end{textblock}}

   872   \only<4>{%

   873   \begin{textblock}{3}(0.6,5.3)

   874   \begin{tikzpicture}

   875   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   876   {\textcolor{red}{a}};

   877   \end{tikzpicture}

   878   \end{textblock}}

   879   \only<5>{%

   880   \begin{textblock}{3}(1.0,5.6)

   881   \begin{tikzpicture}

   882   \node at (0,0) (A) {};

   883   \node at (0,1) (B) {};

   884   \draw[<-, line width=2mm, red] (B) to  (A);

   885   \end{tikzpicture}

   886   \end{textblock}}

   887   \only<5,6>{%

   888   \begin{textblock}{3}(0.6,7.7)

   889   \begin{tikzpicture}

   890   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   891   {\textcolor{red}{a}};

   892   \end{tikzpicture}

   893   \end{textblock}}

   894   \only<6>{%

   895   \begin{textblock}{3}(0.6,10.1)

   896   \begin{tikzpicture}

   897   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

   898   {\textcolor{red}{a}};

   899   \end{tikzpicture}

   900   \end{textblock}}

   901   \only<7>{%

   902   \begin{textblock}{3}(1.0,10.3)

   903   \begin{tikzpicture}

   904   \node at (0,0) (A) {};

   905   \node at (0,1) (B) {};

   906   \draw[->, line width=2mm, red] (B) to  (A);

   907   \end{tikzpicture}

   908   \end{textblock}}

   909 

   910   \end{frame}}

   911   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   912 *}

   913 

   914 

   915 text_raw {*

   916   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   917   \mode<presentation>{

   918   \begin{frame}[c]

   919   \frametitle{\LARGE A Variant of Arden's Lemma}

   920 

   921   {\bf Arden's Lemma:}\smallskip 

   922 

   923   If \smath{[] \not\in A} then

   924   \begin{center}

   925   \smath{X = X; A + \text{something}}

   926   \end{center}

   927   has the (unique) solution

   928   \begin{center}

   929   \smath{X = \text{something} ; A^\star}

   930   \end{center}

   931 

   932 

   933   \end{frame}}

   934   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   935 *}

   936 

   937 

   938 text_raw {*

   939   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   940   \mode<presentation>{

   941   \begin{frame}<1-2,4->[t]

   942   \small

   943 

   944   \begin{center}

   945   \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}ll}

   946   \onslide<1->{\smath{X_1}} & \onslide<1->{\smath{=}} 

   947       & \onslide<1->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   948   \onslide<1->{\smath{X_2}} & \onslide<1->{\smath{=}}    

   949       & \onslide<1->{\smath{X_1; a + X_2; a}}\\

   950 

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

   952 

   953   \onslide<2->{\smath{X_1}} & \onslide<2->{\smath{=}} 

   954       & \onslide<2->{\smath{X_1; b + X_2; b + \lambda;[]}}\\

   955   \onslide<2->{\smath{X_2}} & \onslide<2->{\smath{=}}    

   956       & \only<2->{\smath{X_1; a\cdot a^\star}}\\

   957 

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

   959 

   960   \onslide<4->{\smath{X_1}} & \onslide<4->{\smath{=}} 

   961       & \onslide<4->{\smath{X_2; b \cdot b^\star+ \lambda;b^\star}}\\

   962   \onslide<4->{\smath{X_2}} & \onslide<4->{\smath{=}}    

   963       & \onslide<4->{\smath{X_1; a\cdot a^\star}}\\

   964 

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

   966 

   967   \onslide<5->{\smath{X_1}} & \onslide<5->{\smath{=}} 

   968       & \onslide<5->{\smath{X_1; a\cdot a^\star \cdot b \cdot b^\star+ \lambda;b^\star}}\\

   969   \onslide<5->{\smath{X_2}} & \onslide<5->{\smath{=}}    

   970       & \onslide<5->{\smath{X_1; a\cdot a^\star}}\\

   971 

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

   973 

   974   \onslide<6->{\smath{X_1}} & \onslide<6->{\smath{=}} 

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

   976   \onslide<6->{\smath{X_2}} & \onslide<6->{\smath{=}}    

   977       & \onslide<6->{\smath{X_1; a\cdot a^\star}}\\

   978 

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

   980 

   981   \onslide<7->{\smath{X_1}} & \onslide<7->{\smath{=}} 

   982       & \onslide<7->{\smath{\lambda;b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star}}\\

   983   \onslide<7->{\smath{X_2}} & \onslide<7->{\smath{=}}    

   984       & \onslide<7->{\smath{\lambda; b^\star\cdot (a\cdot a^\star \cdot b \cdot b^\star)^\star 

   985           \cdot a\cdot a^\star}}\\

   986   \end{tabular}

   987   \end{center}

   988 

   989   \only<8->{

   990   \begin{textblock}{6}(2.5,4)

   991   \begin{block}{}

   992   \begin{minipage}{8cm}\raggedright

   993   

   994   \begin{tikzpicture}[shorten >=1pt,node distance=2cm,auto, ultra thick, inner sep=1mm]

   995   \tikzstyle{state}=[circle,thick,draw=blue!75,fill=blue!20,minimum size=0mm]

   996 

   997   %\draw[help lines] (0,0) grid (3,2);

   998 

   999   \node[state,initial]   (p_0)                  {$X_1$};

  1000   \node[state,accepting] (p_1) [right of=q_0]   {$X_2$};

  1001 

  1002   \path[->] (p_0) edge [bend left]   node        {a} (p_1)

  1003                   edge [loop above]   node       {b} ()

  1004             (p_1) edge [loop above]   node       {a} ()

  1005                   edge [bend left]   node        {b} (p_0);

  1006   \end{tikzpicture}

  1007 

  1008   \end{minipage}

  1009   \end{block}

  1010   \end{textblock}}

  1011 

  1012   \only<1,2>{%

  1013   \begin{textblock}{3}(0.6,1.2)

  1014   \begin{tikzpicture}

  1015   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1016   {\textcolor{red}{a}};

  1017   \end{tikzpicture}

  1018   \end{textblock}}

  1019   \only<2>{%

  1020   \begin{textblock}{3}(0.6,3.6)

  1021   \begin{tikzpicture}

  1022   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1023   {\textcolor{red}{a}};

  1024   \end{tikzpicture}

  1025   \end{textblock}}

  1026   \only<4>{%

  1027   \begin{textblock}{3}(0.6,2.9)

  1028   \begin{tikzpicture}

  1029   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1030   {\textcolor{red}{a}};

  1031   \end{tikzpicture}

  1032   \end{textblock}}

  1033   \only<4>{%

  1034   \begin{textblock}{3}(0.6,5.3)

  1035   \begin{tikzpicture}

  1036   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1037   {\textcolor{red}{a}};

  1038   \end{tikzpicture}

  1039   \end{textblock}}

  1040   \only<5>{%

  1041   \begin{textblock}{3}(1.0,5.6)

  1042   \begin{tikzpicture}

  1043   \node at (0,0) (A) {};

  1044   \node at (0,1) (B) {};

  1045   \draw[<-, line width=2mm, red] (B) to  (A);

  1046   \end{tikzpicture}

  1047   \end{textblock}}

  1048   \only<5,6>{%

  1049   \begin{textblock}{3}(0.6,7.7)

  1050   \begin{tikzpicture}

  1051   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1052   {\textcolor{red}{a}};

  1053   \end{tikzpicture}

  1054   \end{textblock}}

  1055   \only<6>{%

  1056   \begin{textblock}{3}(0.6,10.1)

  1057   \begin{tikzpicture}

  1058   \node at (0,0) [single arrow, fill=red,text=white, minimum height=0cm]

  1059   {\textcolor{red}{a}};

  1060   \end{tikzpicture}

  1061   \end{textblock}}

  1062   \only<7>{%

  1063   \begin{textblock}{3}(1.0,10.3)

  1064   \begin{tikzpicture}

  1065   \node at (0,0) (A) {};

  1066   \node at (0,1) (B) {};

  1067   \draw[->, line width=2mm, red] (B) to  (A);

  1068   \end{tikzpicture}

  1069   \end{textblock}}

  1070 

  1071   \end{frame}}

  1072   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1073 *}

  1074 

  1075 

  1076 text_raw {*

  1077   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1078   \mode<presentation>{

  1079   \begin{frame}[c]

  1080   \frametitle{\LARGE The Other Direction}

  1081 

  1082   One has to prove

  1083 

  1084   \begin{center}

  1085   \smath{\text{finite} (U\!N\!IV /\!/ \approx_{{\cal L}(r)})}

  1086   \end{center}

  1087 

  1088   by induction on \smath{r}. Not trivial, but after a bit 

  1089   of thinking, one can find a \alert{refined} relation:\bigskip

  1090 

  1091   

  1092   \begin{center}

  1093   \mbox{\begin{tabular}{c@ {\hspace{7mm}}c@ {\hspace{7mm}}c}

  1094   \begin{tikzpicture}[scale=1.1]

  1095   %Circle

  1096   \draw[thick] (0,0) circle (1.1);    

  1097   \end{tikzpicture}

  1098   &

  1099   \begin{tikzpicture}[scale=1.1]

  1100   %Circle

  1101   \draw[thick] (0,0) circle (1.1);    

  1102   %Main rays

  1103   \foreach \a in {0, 90,...,359}

  1104     \draw[very thick] (0, 0) -- (\a:1.1);

  1105   \foreach \a / \l in {45/1, 135/2, 225/3, 315/4}

  1106       \draw (\a: 0.65) node {\small$a_\l$};

  1107   \end{tikzpicture}

  1108   &

  1109   \begin{tikzpicture}[scale=1.1]

  1110   %Circle

  1111   \draw[red, thick] (0,0) circle (1.1);    

  1112   %Main rays

  1113   \foreach \a in {0, 45,...,359}

  1114      \draw[red, very thick] (0, 0) -- (\a:1.1);

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

  1116       \draw (\a: 0.77) node {\textcolor{red}{\footnotesize$a_{\l}$}};

  1117   \end{tikzpicture}\\

  1118   \small\smath{U\!N\!IV} & 

  1119   \small\smath{U\!N\!IV /\!/ \approx_{{\cal L}(r)}} &

  1120   \small\smath{U\!N\!IV /\!/ \alert{R}}

  1121   \end{tabular}}

  1122   \end{center}

  1123 

  1124   \begin{textblock}{5}(9.8,2.6)

  1125   \begin{tikzpicture}

  1126   \node at (0,0) [shape border rotate=270,single arrow, fill=red,text=white, minimum height=0cm]{\textcolor{red}{a}};

  1127   \end{tikzpicture}

  1128   \end{textblock}

  1129   

  1130 

  1131   \end{frame}}

  1132   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1133 *}

  1134 

  1135 text_raw {*