--- 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:
-