diff -r 7093e600ec2c -r 1769b702d4dc thys/notes.tex
--- a/thys/notes.tex	Fri Jan 30 11:42:53 2015 +0000
+++ b/thys/notes.tex	Fri Jan 30 13:11:39 2015 +0000
@@ -164,7 +164,58 @@
 \]
 
 \noindent
-This is what we need to prove.
+This is what we need to prove. There are only two rules that
+can be used to prove this judgement:
+
+\begin{center}
+\begin{tabular}{cc}
+\begin{tabular}{c}
+$v_1 = v_1'$\qquad $v_2 \succ_{r_2} v_2'$\\
+\hline
+$v_1\cdot v_2 \succ_{r_1\cdot r_2} v_1'\cdot v_2'$
+\end{tabular} &
+\begin{tabular}{c}
+$v_1 \succ_{r_1} v_1'$\\
+\hline
+$v_1\cdot v_2 \succ_{r_1\cdot r_2} v_1'\cdot v_2'$
+\end{tabular}
+\end{tabular}
+\end{center}
+
+\noindent 
+Using the left rule would mean we need to show that
+
+\[
+inj\; r_1\;c\;u_1 = mkeps\;r_1
+\]
+
+\noindent 
+but this can never be the case.\footnote{Actually Isabelle
+found this out after analysing its argument. ;o)} Lets assume
+it would be true, then also if we flat each side, it must hold
+that
+
+\[
+|inj\; r_1\;c\;u_1| = |mkeps\;r_1|
+\]
+
+\noindent 
+But this leads to a contradiction, because the right-hand side
+will be equal to the empty list, or empty string. This is 
+because we assumed $nullable(r_1)$ and there is a lemma
+called \texttt{mkeps\_flat} which shows this. On the other
+side we know by assumption (b***) and lemma \texttt{v4} that 
+the other side needs to be a string starting with $c$ (since
+we inject $c$ into $u_1$). The empty string can never be equal 
+to something starting with $c$\ldots therefore there is a 
+contradiction.
+
+That means we can only use the rule on the right-hand side to 
+prove our goal. This implies we need to prove
+
+\[
+inj\; r_1\;c\;u_1 \succ_{r_1} mkeps\;r_1
+\]
 
 
 \subsubsection*{Case RL}