28 To control the size of regular expressions during derivatives, 

    49 Simplifications are necessary to control the size of regular expressions 

    29 one has to eliminate redundant sub-expression with some

    50 during derivatives by eliminating redundant 

    30 procedure we call $\textit{simp}$, 

    51 sub-expression with some procedure we call $\textit{bsimp}$.

    31 and $\textit{simp}$ is defined as

    52 We want to prove the correctness of $\blexersimp$ which integrates

    32 :

    53 $\textit{bsimp}$ by applying it after each call to the derivative:

    33 

    34 

    35 

    36 Having defined the $\textit{bsimp}$ function,

    37 we add it as a phase after a derivative is taken.

    38 \begin{center}

    39 	\begin{tabular}{lcl}

    40 		$r \backslash_{bsimp} c$ & $\dn$ & $\textit{bsimp}(r \backslash c)$

    41 	\end{tabular}

    42 \end{center}

    43 %Following previous notations

    44 %when extending from derivatives w.r.t.~character to derivative

    45 %w.r.t.~string, we define the derivative that nests simplifications 

    46 %with derivatives:%\comment{simp in  the [] case?}

    47 We extend this from characters to strings:

    50 $r \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(r \backslash_{bsimp}\, c) \backslash_{bsimps}\, s$ \\

    56 	$r \backslash_{bsimps} (c\!::\!s) $ & $\dn$ & $(\textit{bsimp} \; (r \backslash\, c)) \backslash_{bsimps}\, s$ \\

    76 the redundant sub-expressions after each derivative operation

    68 Previously without $\textit{bsimp}$ the exact structure of each intermediate 

    77 allows the exact structure of each intermediate result to be preserved,

    69 regular expression is preserved, allowing pairs of inhabitation relations in the form $\vdash v : r_{c} $ and

    78 so that pairs of inhabitation relations in the form $\vdash v : r_{c} $ and

    70 $\vdash v^{c} : r $ to hold in lemma \ref{retrieveStepwise}(if 

    79 $\vdash v^{c} : r $ hold (if we allow the abbreviation $r_{c} \dn r\backslash c$

    71 we use the convenient notation $r_{c} \dn r\backslash c$

    80 and $v^{c} \dn \inj \;r \; c \; v$).

    72 and $v_{r}^{c} \dn \inj \;r \; c \; v$),

    81 

    73 but $\blexersimp$ introduces simplification after the derivative,

    82 

    74 getting us trouble in aligning the pairs:

    83 Define the 

    75 \begin{center}

    84 But $\blexersimp$ introduces simplification after the derivative

    76 	$\vdash v: \textit{bsimp} \; r_{c} \implies \retrieve \; \textit{bsimp} \; r_c \; v =\retrieve \; r  \;(\mathord{?} v_{r}^{c}) $

    85 to reduce redundancy,

    77 \end{center}

    86 yielding $r \backslash c$ 

    78 \noindent

    87 This allows 

    79 It is quite clear that once we made 

    88 

    80 $v$ to align with $\textit{bsimp} \; r_{c}$

    89 The proof details are necessary materials for this thesis

    81 in the inhabitation relation, something different than $v_{r}^{c}$ needs to be plugged

    90 because it provides necessary context to explain why we need a

    82 in for the above statement to hold.

    91 new framework for the proof of $\blexersimp$, which involves

    83 Ausaf et al. \cite{AusafUrbanDyckhoff2016}

    92 simplifications that cause structural changes to the regular expression.

    84 made some initial attempts on the un-annotated lexer (to be continued)

    93 a new formal proof of the correctness of $\blexersimp$, where the 

    85 

    94 proof of $\blexer$

    95 is not applicatble in the sense that we cannot straightforwardly extend the

    96 proof of theorem \ref{blexerCorrect} because lemma \ref{flex_retrieve} does

    97 not hold anymore.

    98 This is because the structural induction on the stepwise correctness

    99 of $\inj$ breaks due to each pair of $r_i$ and $v_i$ described

   100 in chapter \ref{Inj} and \ref{Bitcoded1} no longer correspond to

   101 each other.

   102 In this chapter we introduce simplifications

   103 for annotated regular expressions that can be applied to 

   104 each intermediate derivative result. This allows

   105 us to make $\blexer$ much more efficient.

   106 Sulzmann and Lu already introduced some simplifications for bitcoded regular expressions,

   107 but their simplification functions could have been more efficient and in some cases needed fixing.