diff -r 1f4e81950ab4 -r 9476086849ad slides/slides11.tex
--- a/slides/slides11.tex	Mon Nov 14 15:50:42 2016 +0000
+++ b/slides/slides11.tex	Sat Jan 07 14:52:26 2017 +0000
@@ -4,12 +4,35 @@
 \usepackage{../data}
 \usepackage{../graphics}
 \usepackage{soul}
-
+\usepackage{proof}
 
 % beamer stuff
 \renewcommand{\slidecaption}{CFL, King's College London}
 \newcommand{\bl}[1]{\textcolor{blue}{#1}}       
 
+\newcommand\grid[1]{%
+	\begin{tikzpicture}[baseline=(char.base)]
+	\path[use as bounding box]
+	(0,0) rectangle (1em,1em);
+	\draw[red!50, fill=red!20]
+	(0,0) rectangle (1em,1em);
+	\node[inner sep=1pt,anchor=base west]
+	(char) at (0em,\gridraiseamount) {#1};
+	\end{tikzpicture}}
+\newcommand\gridraiseamount{0.12em}
+
+\makeatletter
+\newcommand\Grid[1]{%
+	\@tfor\z:=#1\do{\grid{\z}}}
+\makeatother	
+
+\newcommand\Vspace[1][.3em]{%
+	\mbox{\kern.06em\vrule height.3ex}%
+	\vbox{\hrule width#1}%
+	\hbox{\vrule height.3ex}}
+
+\def\VS{\Vspace[0.6em]}
+
 
 \begin{document}
 
@@ -35,6 +58,326 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Compilers \& Boeings 777}
+
+First flight in 1994. They want to achieve triple redundancy in hardware
+faults.\bigskip
+
+They compile 1 Ada program to\medskip
+
+\begin{itemize}
+\item Intel 80486
+\item Motorola 68040 (old Macintosh's)
+\item AMD 29050 (RISC chips used often in laser printers)
+\end{itemize}\medskip
+
+using 3 independent compilers.\bigskip\pause
+
+\small Airbus uses C and static analysers. Recently started using CompCert.
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{seL4 / Isabelle}
+
+\begin{itemize}
+\item verified a microkernel operating system ($\approx$8000 lines of C code)\bigskip
+\item US DoD has competitions to hack into drones; they found that the
+  isolation guarantees of seL4 hold up\bigskip
+\item CompCert and seL4 sell their code  
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{POSIX Matchers}
+
+\begin{itemize}
+\item Longest match rule (``maximal munch rule''): The 
+longest initial substring matched by any regular expression 
+is taken as the next token.
+
+\begin{center}
+\bl{$\texttt{\Grid{iffoo\VS bla}}$}
+\end{center}\medskip
+
+\item Rule priority:
+For a particular longest initial substring, the first regular
+expression that can match determines the token.
+
+\begin{center}
+\bl{$\texttt{\Grid{if\VS bla}}$}
+\end{center}
+\end{itemize}\bigskip\pause
+
+\small
+\hfill Kuklewicz: most POSIX matchers are buggy\\
+\footnotesize
+\hfill \url{http://www.haskell.org/haskellwiki/Regex_Posix}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\mbox{}\\[-14mm]\mbox{}
+\small
+\bl{
+\begin{center}
+\begin{tabular}{lcl}
+$\textit{der}\;c\;(\ZERO)$ & $\dn$ & $\ZERO$\\
+$\textit{der}\;c\;(\ONE)$  & $\dn$ & $\ZERO$\\
+$\textit{der}\;c\;(d)$     & $\dn$ & $\textit{if}\; c = d\;\textit{then} \;\ONE \; \textit{else} \;\ZERO$\\
+$\textit{der}\;c\;(r_1 + r_2)$ & $\dn$ & $(\textit{der}\;c\;r_1) + (\textit{der}\;c\;r_2)$\\
+$\textit{der}\;c\;(r_1 \cdot r_2)$ & $\dn$ & $\textit{if}\;\textit{nullable}(r_1)$\\
+      & & $\textit{then}\;((\textit{der}\;c\;r_1)\cdot r_2) + (\textit{der}\;c\;r_2)$\\
+      & & $\textit{else}\;(\textit{der}\;c\;r_1)\cdot r_2$\\
+$\textit{der}\;c\;(r^*)$ & $\dn$ & $(\textit{der}\;c\;r)\cdot (r^*)$\\
+  $\textit{der}\;c\;(r^{\{n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\
+  & & \textit{else if} $\textit{nullable}(r)$ \textit{then} $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\
+  & & \textit{else} $(\textit{der}\;c\;r)\cdot (r^{\{n-1\}})$\\
+  $\textit{der}\;c\;(r^{\{\uparrow n\}})$ & $\dn$ & \textit{if} $n=0$ \textit{then} $\ZERO$\\
+  & & \textit{else}
+  $(\textit{der}\;c\;r)\cdot (r^{\{\uparrow n-1\}})$\\
+\end{tabular}
+\end{center}}
+  
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t]
+\frametitle{Proofs about Rexps}
+
+Remember their inductive definition:
+
+  \begin{center}
+  \begin{tabular}{@ {}rrl}
+  \bl{$r$} & \bl{$::=$}  & \bl{$\ZERO$}\\
+         & \bl{$\mid$} & \bl{$\ONE$}     \\
+         & \bl{$\mid$} & \bl{$c$}            \\
+         & \bl{$\mid$} & \bl{$r_1 \cdot r_2$}\\
+         & \bl{$\mid$} & \bl{$r_1 + r_2$}    \\
+         & \bl{$\mid$} & \bl{$r^*$}          \\
+         & \bl{$\mid$} & \bl{$r^{\{n\}}$}     \\
+         & \bl{$\mid$} & \bl{$r^{\{\uparrow n\}}$}     \\
+  \end{tabular}
+  \end{center}
+
+If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Proofs about Rexp (2)}
+
+\begin{itemize}
+\item \bl{$P$} holds for \bl{$\ZERO$}, \bl{$\ONE$} and \bl{c}\bigskip
+\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
+holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
+\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
+holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
+\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
+  holds for \bl{$r$}.
+\item \ldots
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Proofs about Strings}
+
+If we want to prove something, say a property \bl{$P(s)$}, for all
+strings \bl{$s$} then \ldots\bigskip
+
+\begin{itemize}
+\item \bl{$P$} holds for the empty string, and\medskip
+\item \bl{$P$} holds for the string \bl{$c\!::\!s$} under the assumption that \bl{$P$}
+already holds for \bl{$s$}
+\end{itemize}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+%\begin{frame}[c]
+%
+%\bl{\begin{center}
+%\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
+%$zeroable(\varnothing)$      & $\dn$ & \textit{true}\\
+%$zeroable(\epsilon)$         & $\dn$ &  \textit{false}\\
+%$zeroable (c)$               & $\dn$ &  \textit{false}\\
+%$zeroable (r_1 + r_2)$       & $\dn$ &  $zeroable(r_1) \wedge zeroable(r_2)$ \\ 
+%$zeroable (r_1 \cdot r_2)$   & $\dn$ &  $zeroable(r_1) \vee zeroable(r_2)$ \\
+%$zeroable (r^*)$             & $\dn$ & \textit{false}\\
+%\end{tabular}
+%\end{center}}
+
+%\begin{center}
+%\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
+%\end{center}
+
+%\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Correctness of the Matcher}
+
+\begin{itemize}
+\item We want to prove\medskip
+\begin{center}
+\bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$}
+\end{center}\bigskip
+
+where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$}
+\bigskip\pause
+
+\item We can do this, if we know\medskip
+\begin{center}
+\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}
+\end{center}
+\end{itemize}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Some Lemmas}
+
+\begin{itemize}
+\item \bl{$Der\;c\;(A\cup B) = 
+(Der\;c\;A)\cup(Der\;c\;B)$}\bigskip
+\item If \bl{$[] \in A$} then
+\begin{center}
+\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$}
+\end{center}\bigskip
+\item If \bl{$[] \not\in A$} then
+\begin{center}
+\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$}
+\end{center}\bigskip
+\item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\
+\small\mbox{}\hfill (interesting case)\\
+\end{itemize}
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{Why?}
+
+Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold?
+\bigskip
+
+
+\begin{center}
+\begin{tabular}{lcl}
+\bl{$Der\;c\;(A^*)$} & \bl{$=$} &  \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\
+& \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\
+& \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\
+& \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\
+\end{tabular}
+\end{center}\bigskip\bigskip
+
+\small
+using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\
+\mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$}
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[c]
+\frametitle{POSIX Spec}
+
+\begin{center}
+\bl{\infer{[] \in \ONE \to Empty}{}}\hspace{15mm}
+\bl{\infer{c \in c \to Char(c)}{}}\bigskip\medskip
+
+\bl{\infer{s \in r_1 + r_2 \to Left(v)}
+          {s \in r_1 \to v}}\hspace{10mm}
+\bl{\infer{s \in r_1 + r_2 \to Right(v)}
+          {s \in r_2 \to v & s \not\in L(r_1)}}\bigskip\medskip
+
+\bl{\infer{s_1 @ s_2 \in r_1 \cdot r_2 \to Seq(v_1, v_2)}
+          {\small\begin{array}{l}
+           s_1 \in r_1 \to v_1 \\
+           s_2 \in r_2 \to v_2 \\
+           \neg(\exists s_3\,s_4.\; s_3 \not= []
+           \wedge s_3 @ s_4 = s_2 \wedge
+           s_1 @ s_3 \in L(r_1) \wedge
+           s_4 \in L(r_2))
+           \end{array}}}
+           
+\bl{\ldots}           
+\end{center}
+
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\begin{frame}[t,squeeze]
+\frametitle{Sulzmann \& Lu Paper}
+
+\begin{itemize}
+\item I have no doubt the algorithm is correct --- 
+  the problem is I do not believe their proof.
+
+  \begin{center}
+  \begin{bubble}[10cm]\small
+  ``How could I miss this? Well, I was rather careless when 
+  stating this Lemma :)\smallskip
+ 
+  Great example how formal machine checked proofs (and 
+  proof assistants) can help to spot flawed reasoning steps.''
+  \end{bubble}
+  \end{center}\pause
+  
+  %\begin{center}
+  %\begin{bubble}[10cm]\small
+  %``Well, I don't think there's any flaw. The issue is how to 
+  %come up with a mechanical proof. In my world mathematical 
+  %proof $=$ mechanical proof doesn't necessarily hold.''
+  %\end{bubble}
+  %\end{center}\pause
+  
+\end{itemize}
+
+  \only<3>{%
+  \begin{textblock}{11}(1,4.4)
+  \begin{center}
+  \begin{bubble}[10.9cm]\small\centering
+  \includegraphics[scale=0.37]{msbug.png}
+  \end{bubble}
+  \end{center}
+  \end{textblock}}
+  
+
+\end{frame}
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% 
+
+\end{document}
+
+%%% Local Variables:  
+%%% mode: latex
+%%% TeX-master: t
+%%% End: 
+
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[t]
 \frametitle{2nd CW}
 
@@ -93,111 +436,6 @@
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
 
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Compilers in Boeings 777}
-
-They want to achieve triple redundancy in hardware
-faults.\bigskip
-
-They compile 1 Ada program to
-
-\begin{itemize}
-\item Intel 80486
-\item Motorola 68040 (old Macintosh's)
-\item AMD 29050 (RISC chips used often in laser printers)
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[t]
-\frametitle{Proofs about Rexps}
-
-Remember their inductive definition:
-
-  \begin{center}
-  \begin{tabular}{@ {}rrl}
-  \bl{$r$} & \bl{$::=$}  & \bl{$\varnothing$}\\
-         & \bl{$\mid$} & \bl{$\epsilon$}     \\
-         & \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{center}
-
-If we want to prove something, say a property \bl{$P(r)$}, for all regular expressions \bl{$r$} then \ldots
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Proofs about Rexp (2)}
-
-\begin{itemize}
-\item \bl{$P$} holds for \bl{$\varnothing$}, \bl{$\epsilon$} and \bl{c}\bigskip
-\item \bl{$P$} holds for \bl{$r_1 + r_2$} under the assumption that \bl{$P$} already
-holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
-\item \bl{$P$} holds for \bl{$r_1 \cdot r_2$} under the assumption that \bl{$P$} already
-holds for \bl{$r_1$} and \bl{$r_2$}.\bigskip
-\item \bl{$P$} holds for \bl{$r^*$} under the assumption that \bl{$P$} already
-holds for \bl{$r$}.
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-
-\bl{\begin{center}
-\begin{tabular}{@ {}l@ {\hspace{2mm}}c@ {\hspace{2mm}}l@ {}}
-$zeroable(\varnothing)$      & $\dn$ & \textit{true}\\
-$zeroable(\epsilon)$         & $\dn$ &  \textit{false}\\
-$zeroable (c)$               & $\dn$ &  \textit{false}\\
-$zeroable (r_1 + r_2)$       & $\dn$ &  $zeroable(r_1) \wedge zeroable(r_2)$ \\ 
-$zeroable (r_1 \cdot r_2)$   & $\dn$ &  $zeroable(r_1) \vee zeroable(r_2)$ \\
-$zeroable (r^*)$             & $\dn$ & \textit{false}\\
-\end{tabular}
-\end{center}}
-
-\begin{center}
-\bl{$zeroable(r)$} if and only if \bl{$L(r) = \{\}$}
-\end{center}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Correctness of the Matcher}
-
-\begin{itemize}
-\item We want to prove\medskip
-\begin{center}
-\bl{$matches\;r\;s$} if and only if \bl{$s\in L(r)$}
-\end{center}\bigskip
-
-where \bl{$matches\;r\;s \dn nullable(ders\;s\;r)$}
-\bigskip\pause
-
-\item We can do this, if we know\medskip
-\begin{center}
-\bl{$L(der\;c\;r) = Der\;c\;(L(r))$}
-\end{center}
-\end{itemize}
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 \begin{frame}[c]
 \frametitle{Induction over Strings}
@@ -258,60 +496,3 @@
 
 \end{frame}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Some Lemmas}
-
-\begin{itemize}
-\item \bl{$Der\;c\;(A\cup B) = 
-(Der\;c\;A)\cup(Der\;c\;B)$}\bigskip
-\item If \bl{$[] \in A$} then
-\begin{center}
-\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B \;\cup\; (Der\;c\;B)$}
-\end{center}\bigskip
-\item If \bl{$[] \not\in A$} then
-\begin{center}
-\bl{$Der\;c\;(A\,@\,B) = (Der\;c\;A)\,@\,B$}
-\end{center}\bigskip
-\item \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$}\\
-\small\mbox{}\hfill (interesting case)\\
-\end{itemize}
-
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\begin{frame}[c]
-\frametitle{Why?}
-
-Why does \bl{$Der\;c\;(A^*) = (Der\;c\;A)\,@\,A^*$} hold?
-\bigskip
-
-
-\begin{center}
-\begin{tabular}{lcl}
-\bl{$Der\;c\;(A^*)$} & \bl{$=$} &  \bl{$Der\;c\;(A^* - \{[]\})$}\medskip\\
-& \bl{$=$} & \bl{$Der\;c\;((A - \{[]\})\,@\,A^*)$}\medskip\\
-& \bl{$=$} & \bl{$(Der\;c\;(A - \{[]\}))\,@\,A^*$}\medskip\\
-& \bl{$=$} & \bl{$(Der\;c\;A)\,@\,A^*$}\medskip\\
-\end{tabular}
-\end{center}\bigskip\bigskip
-
-\small
-using the facts \bl{$Der\;c\;A = Der\;c\;(A - \{[]\})$} and\\
-\mbox{}\hfill\bl{$(A - \{[]\}) \,@\, A^* = A^* - \{[]\}$}
-\end{frame}
-%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   
-
-
-
-\end{document}
-
-%%% Local Variables:  
-%%% mode: latex
-%%% TeX-master: t
-%%% End: 
-