diff -r 434ba43d0430 -r 2cdbab037861 thys/notes.tex
--- a/thys/notes.tex	Fri Jan 30 13:19:15 2015 +0000
+++ b/thys/notes.tex	Sat Jan 31 18:21:03 2015 +0000
@@ -1,11 +1,127 @@
 \documentclass[11pt]{article}
 \usepackage[left]{lineno}
+\usepackage{amsmath}
 
 \begin{document}
-\linenumbers
+%%\linenumbers
+
+\noindent 
+We already proved that
+
+\[
+\text{If}\;nullable(r)\;\text{then}\;POSIX\;(mkeps\; r)\;r
+\]
+
+\noindent 
+holds. This is essentially the ``base case'' for the
+correctness proof of the algorithm. For the ``induction
+case'' we need the following main theorem, which we are 
+currently after:
+
+\begin{center}
+\begin{tabular}{lll}
+If & (*) & $POSIX\;v\;(der\;c\;r)$ and $\vdash v : der\;c\;r$\\
+then & & $POSIX\;(inj\;r\;c\;v)\;r$
+\end{tabular}
+\end{center}
+
+\noindent 
+That means a POSIX value $v$ is still $POSIX$ after injection.
+I am not sure whether this theorem is actually true in this
+full generality. Maybe it requires some restrictions.
+
+If we unfold the $POSIX$ definition in the then-part, we 
+arrive at
+
+\[
+\forall v'.\;
+\text{if}\;\vdash v' : r\; \text{and} \;|inj\;r\;c\;v| = |v'|\;
+\text{then}\; |inj\;r\;c\;v| \succ_r v' 
+\]
+
+\noindent 
+which is what we need to prove assuming the if-part (*) in the
+theorem above. Since this is a universally quantified formula,
+we just need to fix a $v'$. We can then prove the implication
+by assuming
+
+\[
+\text{(a)}\;\;\vdash v' : r\;\; \text{and} \;\;
+\text{(b)}\;\;inj\;r\;c\;v = |v'|
+\]
+
+\noindent 
+and our goal is
+
+\[
+(goal)\;\;inj\;r\;c\;v \succ_r v'
+\]
+
+\noindent 
+There are already two lemmas proved that can transform 
+the assumptions (a) and (b) into
 
-\noindent
-A lemma which might be true, but can also be false, is as follows:
+\[
+\text{(a*)}\;\;\vdash proj\;r\;c\;v' : der\;c\;r\;\; \text{and} \;\;
+\text{(b*)}\;\;c\,\#\,|v| = |v'|
+\]
+
+\noindent 
+Another lemma shows that
+
+\[
+|v'| = c\,\#\,|proj\;r\;c\;v|
+\]
+
+\noindent 
+Using (b*) we can therefore infer 
+
+\[
+\text{(b**)}\;\;|v| = |proj\;r\;c\;v|
+\]
+
+\noindent 
+The main idea of the proof is now a simple instantiation
+of the assumption $POSIX\;v\;(der\;c\;r)$. If we unfold 
+the $POSIX$ definition, we get
+
+\[
+\forall v'.\;
+\text{if}\;\vdash v' : der\;c\;r\; \text{and} \;|v| = |v'|\;
+\text{then}\; v \succ_{der\;c\;r}\; v' 
+\]
+
+\noindent 
+We can instantiate this $v'$ with $proj\;r\;c\;v'$ and can use 
+(a*) and (b**) in order to infer
+
+\[
+v \succ_{der\;c\;r}\; proj\;r\;c\;v'
+\]
+
+\noindent 
+The point of the side-lemma below is that we can ``add'' an
+$inj$ to both sides to obtain
+
+\[
+inj\;r\;c\;v \succ_r\; inj\;r\;c\;(proj\;r\;c\;v')
+\]
+
+\noindent Finally there is already a lemma proved that shows
+that an injection and projection is the identity, meaning
+
+\[
+inj\;r\;c\;(proj\;r\;c\;v') = v'
+\]
+
+\noindent 
+With this we have shown our goal (pending a proof of the side-lemma 
+next).
+
+
+\subsection*{Side-Lemma}
+
+A side-lemma needed for the theorem above which might be true, but can also be false, is as follows:
 
 \begin{center}
 \begin{tabular}{lll}