1 \documentclass[11pt]{article}

     2 

     3 \begin{document}

     4 

     5 \noindent

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

     7 

     8 \begin{center}

     9 \begin{tabular}{lll}

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

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

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

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

    14 \end{tabular}

    15 \end{center}

    16 

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

    18 bigger than $v_2$ then this ordering is preserved under 

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

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

    21 \bigskip

    22 

    23 \noindent

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

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

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

    27 

    28 \begin{center}

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

    30 \end{center}

    31 

    32 \noindent 

    33 or without the parentheses

    34 

    35 \begin{center}

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

    37 \end{center}

    38 

    39 \noindent 

    40 In this case the assumptions are

    41 

    42 \begin{center}

    43 \begin{tabular}{ll}

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

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

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

    47 (d) & $nullable(r_1)$

    48 \end{tabular}

    49 \end{center}

    50 

    51 \noindent 

    52 The induction hypotheses are

    53 

    54 \begin{center}

    55 \begin{tabular}{ll}

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

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

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

    59       & $\hfill\longrightarrow

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

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

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

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

    64       & $\hfill\longrightarrow

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

    66 \end{tabular}

    67 \end{center}

    68 

    69 \noindent 

    70 The goal is

    71 

    72 \[

    73 (goal)\qquad

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

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

    76 \]

    77 

    78 \noindent 

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

    80 distinction), then we will find four cases:

    81 

    82 \begin{center}

    83 \begin{tabular}{ll}

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

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

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

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

    88 \end{tabular}

    89 \end{center}

    90 

    91 

    92 \noindent 

    93 We have to establish our goal in all four cases. 

    94 

    95 

    96 \subsubsection*{Case LR}

    97 

    98 The corresponding rule (instantiated) is:

    99 

   100 \begin{center}

   101 \begin{tabular}{c}

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

   103 \hline

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

   105 \end{tabular}

   106 \end{center}

   107 

   108 \subsubsection*{Case RL}

   109 

   110 The corresponding rule (instantiated) is:

   111 

   112 \begin{center}

   113 \begin{tabular}{c}

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

   115 \hline

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

   117 \end{tabular}

   118 \end{center}

   119 

   120 

   121 \end{document}