diff -r f702fd716bd8 -r 32af6d4de262 proof.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/proof.tex	Fri Oct 05 00:40:52 2012 +0100
@@ -0,0 +1,140 @@
+\documentclass{article}
+\usepackage{charter}
+\usepackage{hyperref}
+\usepackage{amssymb}
+\usepackage{amsmath}
+
+\newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}% for definitions
+\begin{document}
+
+\section*{Proof}
+
+Recall the definitions for regular expressions and the language associated with a regular expression:
+
+\begin{center}
+\begin{tabular}{c}
+\begin{tabular}[t]{rcl}
+  $r$ & $::=$  & $\varnothing$  \\
+         & $\mid$ & $\epsilon$       \\
+         & $\mid$ & $c$                         \\
+         & $\mid$ & $r_1 \cdot r_2$ \\
+         & $\mid$ & $r_1 + r_2$  \\
+         & $\mid$ & $r^*$                 \\
+  \end{tabular}\hspace{10mm}
+\begin{tabular}[t]{r@{\hspace{1mm}}c@{\hspace{1mm}}l}
+$L(\varnothing)$ & $\dn$ & $\varnothing$ \\
+$L(\epsilon)$       & $\dn$ & $\{\texttt{""}\}$       \\
+$L(c)$                   & $\dn$ & $\{\texttt{"}c\texttt{"}\}$                         \\
+$L(r_1 \cdot r_2)$   & $\dn$ & $L(r_1) \,@\, L(r_2)$ \\
+$L(r_1 + r_2)$         & $\dn$ & $L(r_1) \cup L(r_2)$  \\
+ $L(r^*)$        & $\dn$ & $\bigcup_{n\ge 0} L(r)^n$                 \\
+  \end{tabular}
+\end{tabular}
+\end{center}
+
+\noindent
+We also defined the notion of a derivative of a regular expression (the derivative with respect to a character):
+
+\begin{center}
+\begin{tabular}{lcl}
+  $der\, c\, (\varnothing)$    & $\dn$ & $\varnothing$  \\
+  $der\, c\, (\epsilon)$          & $\dn$ & $\varnothing$ \\
+  $der\, c\, (d)$                      & $\dn$ & if $c = d$ then $\epsilon$ else $\varnothing$\\
+  $der\, c\, (r_1 + r_2)$        & $\dn$ & $(der\, c\, r_1) + (der\, c\, r_2)$ \\
+  $der\, c\, (r_1 \cdot r_2)$ & $\dn$  & if $nullable(r_1)$\\
+       & & then $((der\, c\, r_1) \cdot r_2) + (der\, c\, r_2)$\\ 
+       & & else $(der\, c\, r_1) \cdot r_2$\\
+  $der\, c\, (r^*)$                   & $\dn$ & $(der\, c\, r) \cdot (r^*)$\\
+  \end{tabular}
+\end{center}
+
+\noindent
+With our definition of regular expressions comes an induction principle. Given a property $P$ over 
+regular expressions. We can establish that $\forall r.\; P(r)$ holds, provided we can show the following:
+
+\begin{enumerate}
+\item $P(\varnothing)$, $P(\epsilon)$ and $P(c)$ all hold,
+\item $P(r_1 + r_2)$ holds under the induction hypotheses that 
+$P(r_1)$ and $P(r_2)$ hold,
+\item $P(r_1 \cdot r_2)$ holds under the induction hypotheses that 
+$P(r_1)$ and $P(r_2)$ hold, and
+\item $P(r^*)$ holds under the induction hypothesis that $P(r)$ holds.
+\end{enumerate}
+
+\noindent
+Let us try out an induction proof. Recall the definition
+
+\begin{center}
+$Der\, c\, A \dn \{ s\;\mid\; c\!::\!s \in A\}$
+\end{center}
+
+\noindent
+whereby $A$ is a set of strings. We like to prove
+
+\begin{center}
+\begin{tabular}{l}
+$P(r) \dn $ \hspace{4mm} $L(der\,c\,r) = Der\,c\,(L(r))$
+\end{tabular}
+\end{center}
+
+\noindent
+by induction over the regular expression $r$.
+
+
+\newpage
+\noindent
+{\bf Proof}
+
+\noindent
+According to 1.~above we need to prove $P(\varnothing)$, $P(\epsilon)$ and $P(d)$. Lets do this in turn.
+
+\begin{itemize}
+\item First Case: $P(\varnothing)$ is $L(der\,c\,\varnothing) = Der\,c\,(L(\varnothing))$ (a). We have $der\,c\,\varnothing = \varnothing$ 
+and $L(\varnothing) = \varnothing$. We also have $Der\,c\,\varnothing = \varnothing$. Hence we have $\varnothing = \varnothing$ in (a). 
+
+\item Second  Case: $P(\epsilon)$ is $L(der\,c\,\epsilon) = Der\,c\,(L(\epsilon))$ (b). We have $der\,c\,\epsilon = \varnothing$,
+$L(\varnothing) = \varnothing$ and $L(\epsilon) = \{\texttt{""}\}$. We also have $Der\,c\,\{\texttt{""}\} = \varnothing$. Hence we have 
+$\varnothing = \varnothing$ in (b). 
+
+\item Third  Case: $P(d)$ is $L(der\,c\,d) = Der\,c\,(L(d))$ (c). We need to treat the cases $d = c$ and $d \not= c$. 
+
+$d = c$: We have $der\,c\,c = \epsilon$ and $L(\epsilon) = \{\texttt{""}\}$. 
+We also have $L(c) = \{\texttt{"}c\texttt{"}\}$ and $Der\,c\,\{\texttt{"}c\texttt{"}\} = \{\texttt{""}\}$. Hence we have 
+$\{\texttt{""}\} = \{\texttt{""}\}$ in (c). 
+
+$d \not=c$: We have $der\,c\,d = \varnothing$.
+We also have $Der\,c\,\{\texttt{"}d\texttt{"}\} = \varnothing$. Hence we have 
+$\varnothing = \varnothing$  in (c). 
+
+\item Fourth Case: $P(r_1 + r_2)$ is $L(der\,c\,(r_1 + r_2)) = Der\,c\,(L(r_1 + r_2))$ (d). This is what we have to show.
+We can assume already:
+
+\begin{center}
+\begin{tabular}{ll}
+$P(r_1)$: & $L(der\,c\,r_1) = Der\,c\,(L(r_1))$ (I)\\
+$P(r_2)$: & $L(der\,c\,r_2) = Der\,c\,(L(r_2))$ (II)
+\end{tabular}
+\end{center}
+
+We have that $der\,c\,(r_1 + r_2) = (der\,c\,r_1) + (der\,c\,r_2)$ and also $L((der\,c\,r_1) + (der\,c\,r_2)) = L(der\,c\,r_1) \cup L(der\,c\,r_2)$.
+By (I) and (II) we know that the left-hand side is $Der\,c\,(L(r_1)) \cup Der\,c\,(L(r_2))$.  You need to ponder a bit, but you should see
+that 
+
+\begin{center}
+$Der\,c(A \cup B) = (Der\,c\,A) \cup (Der\,c\,B)$
+\end{center}
+
+holds for every set of strings $A$ and $B$. That means the right-hand side of (d) is also $Der\,c\,(L(r_1)) \cup Der\,c\,(L(r_2))$,
+because $L(r_1 + r_2) = L(r_1) \cup L(r_2)$. And we are done with the fourth case.
+ 
+\item Fifth Case:
+
+\item Sixth Case:
+\end{itemize}
+
+\end{document}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: t
+%%% End: