167 This is what we need to prove.

   167 This is what we need to prove. There are only two rules that

   168 can be used to prove this judgement:

   169 

   170 \begin{center}

   171 \begin{tabular}{cc}

   172 \begin{tabular}{c}

   173 $v_1 = v_1'$\qquad $v_2 \succ_{r_2} v_2'$\\

   174 \hline

   175 $v_1\cdot v_2 \succ_{r_1\cdot r_2} v_1'\cdot v_2'$

   176 \end{tabular} &

   177 \begin{tabular}{c}

   178 $v_1 \succ_{r_1} v_1'$\\

   179 \hline

   180 $v_1\cdot v_2 \succ_{r_1\cdot r_2} v_1'\cdot v_2'$

   181 \end{tabular}

   182 \end{tabular}

   183 \end{center}

   184 

   185 \noindent 

   186 Using the left rule would mean we need to show that

   187 

   188 \[

   189 inj\; r_1\;c\;u_1 = mkeps\;r_1

   190 \]

   191 

   192 \noindent 

   193 but this can never be the case.\footnote{Actually Isabelle

   194 found this out after analysing its argument. ;o)} Lets assume

   195 it would be true, then also if we flat each side, it must hold

   196 that

   197 

   198 \[

   199 |inj\; r_1\;c\;u_1| = |mkeps\;r_1|

   200 \]

   201 

   202 \noindent 

   203 But this leads to a contradiction, because the right-hand side

   204 will be equal to the empty list, or empty string. This is 

   205 because we assumed $nullable(r_1)$ and there is a lemma

   206 called \texttt{mkeps\_flat} which shows this. On the other

   207 side we know by assumption (b***) and lemma \texttt{v4} that 

   208 the other side needs to be a string starting with $c$ (since

   209 we inject $c$ into $u_1$). The empty string can never be equal 

   210 to something starting with $c$\ldots therefore there is a 

   211 contradiction.

   212 

   213 That means we can only use the rule on the right-hand side to 

   214 prove our goal. This implies we need to prove

   215 

   216 \[

   217 inj\; r_1\;c\;u_1 \succ_{r_1} mkeps\;r_1

   218 \]