# HG changeset patch
# User urbanc
# Date 1314173022 0
# Node ID a9e4acbf7b0056512617bbf5e7e7bfb001dd6dc1
# Parent  580e0632917147a3493f6b73db66ea87cba4bf63
more on slides

diff -r 580e06329171 -r a9e4acbf7b00 Slides/Slides1.thy
--- a/Slides/Slides1.thy	Wed Aug 24 07:24:22 2011 +0000
+++ b/Slides/Slides1.thy	Wed Aug 24 08:03:42 2011 +0000
@@ -13,7 +13,9 @@
 text_raw {*
   %\renewcommand{\slidecaption}{Cambridge, 9 November 2010}
   \renewcommand{\slidecaption}{Nijmegen, 25 August 2011}
-  \renewcommand{\ULthickness}{2pt}
+  %%\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}
@@ -32,7 +34,6 @@
   \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
@@ -58,8 +59,8 @@
   \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 (induction).
+  \large I want to teach \alert{students} with\\ 
+  theorem provers (especially inductions).
   \end{minipage}
   \end{block}
   \end{textblock}\pause
@@ -68,8 +69,7 @@
 
   \begin{itemize}
   \item \only<2>{\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}%
-        \only<3->{\textcolor{red}{\sout{\textcolor{black}%
-        {\smath{\text{fib}}, \smath{\text{even}} and \smath{\text{odd}}}}}}\medskip
+        \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}
@@ -217,7 +217,7 @@
 
   \only<6->{A solution:\;\;\smath{\text{nat}} \;@{text "\<Rightarrow>"}\; state nodes\medskip}
 
-  \only<7->{You have to \alert{\uline{rename}} states!}
+  \only<7->{You have to \alert{\underline{rename}} states!}
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -261,7 +261,7 @@
   {\bf Definition:}\smallskip\\
   
   A language \smath{A} is \alert{regular}, provided there exists a\\ 
-  regular expression that matches all strings of \smath{A}.
+  \alert{regular expression} that matches all strings of \smath{A}.
   \end{minipage}
   \end{block}
   \end{textblock}\pause
@@ -273,7 +273,7 @@
   \item pumping lemma\pause
   \item closure under complementation\pause
   \item \only<6>{regular expression matching}%
-  \only<7->{\textcolor{red}{\sout{\textcolor{black}{regular expression matching}}}}
+       \only<7->{\sout{regular expression matching}}
   \item<8-> most textbooks are about automata
   \end{itemize}
 
@@ -291,8 +291,8 @@
   \frametitle{\LARGE The Myhill-Nerode Theorem}
 
   \begin{itemize}
-  \item provides necessary and suf\!ficient conditions for a language 
-  being regular (pumping lemma only necessary)\medskip
+  \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
 
@@ -413,8 +413,7 @@
   \begin{frame}[c]
   \frametitle{\LARGE Systems of Equations}
 
-  Inspired by a method of Brzozowski\;'64, we can build an equational system
-  characterising the equivalence classes:
+  Inspired by a method of Brzozowski\;'64:\bigskip\bigskip
 
   \begin{center}
   \begin{tabular}{@ {\hspace{-20mm}}c}
@@ -447,10 +446,11 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+
 text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
-  \begin{frame}<1>[t]
+  \begin{frame}<1-2,4->[t]
   \small
 
   \begin{center}
@@ -465,87 +465,7 @@
   \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 + R_2; a}}%
-        \only<3->{\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}
-
-  \end{frame}}
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
-*}
-
-text_raw {*
-  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-  \mode<presentation>{
-  \begin{frame}[c]
-  \frametitle{\LARGE A Variant of Arden's Lemma}
-
-  {\bf ``Reversed'' Arden's Lemma:}\medskip 
-
-  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->[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 + R_2; a}}%
-        \only<3->{\smath{R_1; a\cdot a^\star}}\\
+      & \only<2->{\smath{R_1; a\cdot a^\star}}\\
 
   & & & \onslide<4->{by Arden}\\
 
@@ -719,7 +639,7 @@
   \frametitle{\LARGE Conclusion}
 
   \begin{itemize}
-  \item We have never ever seen a proof of Myhill-Nerode based on
+  \item We have never seen a proof of Myhill-Nerode based on
   regular expressions.\smallskip\pause
 
   \item great source of examples (inductions)\smallskip\pause
diff -r 580e06329171 -r a9e4acbf7b00 Slides/document/root.tex
--- a/Slides/document/root.tex	Wed Aug 24 07:24:22 2011 +0000
+++ b/Slides/document/root.tex	Wed Aug 24 08:03:42 2011 +0000
@@ -1,4 +1,5 @@
 \usepackage{beamerthemeplaincu}
+%%\usepackage{ulem}
 \usepackage[T1]{fontenc}
 \usepackage{proof}
 \usepackage[latin1]{inputenc}
@@ -9,7 +10,6 @@
 \usepackage{proof}
 \usepackage{ifthen}
 \usepackage{animate}
-\usepackage{ulem}
 \usepackage{tikz}
 \usepackage{pgf}
 \usetikzlibrary{arrows}