diff -r 7b78e093f559 -r 2d30c74ba67f thys/notes.tex
--- a/thys/notes.tex	Thu Feb 26 12:51:02 2015 +0000
+++ b/thys/notes.tex	Thu Feb 26 16:35:10 2015 +0000
@@ -3,7 +3,7 @@
 \usepackage{amsmath}
 
 \begin{document}
-%%\linenumbers
+%%%\linenumbers
 
 \noindent 
 We already proved that
@@ -348,6 +348,33 @@
 \end{tabular}
 \end{center}
 
+\subsection*{Test Proof}
+
+We want to prove that
+
+\[
+nullable(r) \;\text{implies}\; POSIX (mkeps\; r)\; r
+\]
+
+\noindent
+We prove this by induction on $r$. There are 5 subcases, and 
+only the $r_1 + r_2$-case is interesting. In this case we know the 
+induction hypotheses are
+
+\begin{center}
+\begin{tabular}{ll}
+(IMP1) & $nullable(r_1) \;\text{implies}\; 
+          POSIX (mkeps\; r_1)\; r_1$ \\
+(IMP2) & $nullable(r_2) \;\text{implies}\;
+          POSIX (mkeps\; r_2)\; r_2$
+\end{tabular}
+\end{center}
+
+\noindent and know that $nullable(r_1 + r_2)$ holds. From this
+we know that either $nullable(r_1)$ holds or $nullable(r_2)$.
+Let us consider the first case where we know $nullable(r_1)$.
+
+
 \subsection*{Problems in the paper proof}
 
 I cannot verify