\documentclass[11pt]{article}

\begin{document}

\noindent

A lemma which might be true, but can also be false, is as follows:

\begin{center}

\begin{tabular}{lll}

If   & (1) & $v_1 \succ_{der\;c\;r} v_2$,\\

     & (2) & $\vdash v_1 : der\;c\;r$, and\\ 

     & (3) & $\vdash v_2 : der\;c\;r$ holds,\\

then &     & $inj\;r\;c\;v_1 \succ_r inj\;r\;c\;v_2$ also holds.  

\end{tabular}

\end{center}

\noindent It essentially states that if one value $v_1$ is 

bigger than $v_2$ then this ordering is preserved under 

injections. This is proved by induction (on the definition of 

$der$\ldots this is very similar to an induction on $r$).

\bigskip

\noindent

The case that is still unproved is the sequence case where we 

assume $r = r_1\cdot r_2$ and also $r_1$ being nullable.

The derivative $der\;c\;r$ is then

\begin{center}

$der\;c\;r = ((der\;c\;r_1) \cdot r_2) + (der\;c\;r_2)$

\end{center}

\noindent 

or without the parentheses

\begin{center}

$der\;c\;r = (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$

\end{center}

\noindent 

In this case the assumptions are

\begin{center}

\begin{tabular}{ll}

(a) & $v_1 \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} v_2$\\

(b) & $\vdash v_1 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\

(c) & $\vdash v_2 : (der\;c\;r_1) \cdot r_2 + der\;c\;r_2$\\

(d) & $nullable(r_1)$

\end{tabular}

\end{center}

\noindent 

The induction hypotheses are

\begin{center}

\begin{tabular}{ll}

(IH1) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_1} v_2

\;\wedge\; \vdash v_1 : der\;c\;r_1 \;\wedge\; 

\vdash v_2 : der\;c\;r_1\qquad$\\

      & $\hfill\longrightarrow

         inj\;r_1\;c\;v_1 \succ{r_1} \;inj\;r_1\;c\;v_2$\smallskip\\

(IH2) & $\forall v_1 v_2.\;v_1 \succ_{der\;c\;r_2} v_2

\;\wedge\; \vdash v_2 : der\;c\;r_2 \;\wedge\; 

\vdash v_2 : der\;c\;r_2\qquad$\\

      & $\hfill\longrightarrow

         inj\;r_2\;c\;v_1 \succ{r_2} \;inj\;r_2\;c\;v_2$\\

\end{tabular}

\end{center}

\noindent 

The goal is

\[

(goal)\qquad

inj\; (r_1 \cdot r_2)\;c\;v_1 \succ_{r_1 \cdot r_2} 

inj\; (r_1 \cdot r_2)\;c\;v_2

\]

\noindent 

If we analyse how (a) could have arisen (that is make a case

distinction), then we will find four cases:

\begin{center}

\begin{tabular}{ll}

LL & $v_1 = Left(w_1)$, $v_2 = Left(w_2)$\\

LR & $v_1 = Left(w_1)$, $v_2 = Right(w_2)$\\

RL & $v_1 = Right(w_1)$, $v_2 = Left(w_2)$\\

RR & $v_1 = Right(w_1)$, $v_2 = Right(w_2)$\\

\end{tabular}

\end{center}

\noindent 

We have to establish our goal in all four cases. 

\subsubsection*{Case LR}

The corresponding rule (instantiated) is:

\begin{center}

\begin{tabular}{c}

$len\,|w_1| \geq len\,|w_2|$\\

\hline

$Left(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Right(w_2)$

\end{tabular}

\end{center}

\subsubsection*{Case RL}

The corresponding rule (instantiated) is:

\begin{center}

\begin{tabular}{c}

$len\,|w_1| > len\,|w_2|$\\

\hline

$Right(w_1) \succ_{(der\;c\;r_1) \cdot r_2 + der\;c\;r_2} Left(w_2)$

\end{tabular}

\end{center}

\end{document}