875 where originally only one step was needed.

   875 where originally only one step was needed:

   877 	$r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$ 

   877 	\hspace{0em}

   878 	and

   878 	\begin{itemize}

   879 	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies 

   879 		\item

   880 	\map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$

   880 			If $r_1 \rightsquigarrow r_2$, then $r_1 \backslash c 

   881 \end{lemma}

   881 			\rightsquigarrow^*  r_2 \backslash c$ 

   882 \begin{proof}

   882 		\item	

   883 	By induction on $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.

   883 			If $rs_1 \stackrel{s}{\rightsquigarrow} rs_2$, then $ 

   884 \end{proof}

   884 			\map \; (\_\backslash c) \; rs_1 

   885 Now we can prove that once we could rewrite from one expression to another in many steps,

   885 			\stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$

   886 then after a derivative on both sides we could still rewrite one to another in many steps:

   886 	\end{itemize}

   887 \begin{lemma}

   887 \end{lemma}

   888 	$r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$

   888 \begin{proof}

   889 \end{lemma}

   889 	By induction on $\rightsquigarrow$ 

   890 \begin{proof}

   890 	and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.

   891 	By rule induction of $\stackrel{*}{\rightsquigarrow} $ and using the previous lemma :\ref{rewriteBder}.

   891 \end{proof}

   892 \end{proof}

   892 \noindent

   893 \noindent

   893 Now we can prove property 3, as an immediate corollary:

   894 This can be extended and combined with the previous two important properties

   894 \begin{corollary}\label{rewritesBder}

   895 so that a regular expression's successivve derivatives can be rewritten in many steps

   895 	$r_1 \rightsquigarrow^* r_2 \implies r_1 \backslash c \rightsquigarrow^*   

   896 to its simplified counterpart:

   896 	r_2 \backslash c$

   897 \end{corollary}

   898 \begin{proof}

   899 	By rule induction of $\stackrel{*}{\rightsquigarrow} $ and using the previous lemma \ref{rewriteBder}.

   900 \end{proof}

   901 \noindent

   902 This can be extended and combined with $r \rightsquigarrow^* \textit{bsimp} \; r$

   903 to obtain the rewritability between

   904 $\blexer$ and $\blexersimp$'s intermediate

   905 derivative regular expressions 

   898 	$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $

   907 	$a \backslash s \rightsquigarrow^* \bderssimp{a}{s} $

   899 \end{lemma}

   908 \end{lemma}

   909 \begin{proof}

   910 	By an induction on $s$.

   911 \end{proof}

   901 Now with \ref{bdersBderssimp} we are ready for the main theorem.

   913 Now with \ref{bderBderssimp} we are ready for the main theorem.

   902 To link $\blexersimp$ and $\blexer$, 

   903 we first say that they give out the same bits, if the lexing result is a match:

   904 \begin{lemma}

   905 	$\bnullable \; (a \backslash s) \implies \bmkeps \; (a \backslash s) = \bmkeps \; (\bderssimp{a}{s})$

   906 \end{lemma}

   907 \noindent

   908 Now that they give out the same bits, we know that they give the same value after decoding,

   909 which we know is correct value as $\blexer$ is correct:

   915 	One can rewrite in many steps from the original lexer's derivative regular expressions to the 

   919 	One can rewrite in many steps from the original lexer's 

   916 	lexer with simplification applied:

   920 	derivative regular expressions to the 

   917 	$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.

   921 	lexer with simplification applied (by lemma \ref{bderBderssimp}):

   918 	If two regular expressions are rewritable, then they produce the same bits.

   922 	\begin{center}

   919 	Under the condition that $ r_1$ is nullable, we have

   923 		$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.

   920 	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$.

   924 	\end{center}

   921 	We have that 

   925 	we know that they give out the same bits, if the lexing result is a match:

   922 	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$ holds.

   926 	\begin{center}

   923 	This proves the \emph{if}  branch of

   927 		$\bnullable \; (a \backslash s) 

   924 	$\blexer \; r \; s = \blexersimp{r}{s}$.

   928 		\implies \bmkeps \; (a \backslash s) = \bmkeps \; (\bderssimp{a}{s})$

   925 

   929 	\end{center}

   930 	Now that they give out the same bits, we know that they give the same value after decoding.

   931 	\begin{center}

   932 		$\bnullable \; (a \backslash s) 

   933 		\implies \decode \; r \; (\bmkeps \; (a \backslash s)) = 

   934 		\decode \; r \; (\bmkeps \; (\bderssimp{a}{s}))$

   935 	\end{center}

   936 	Which is equivalent to our proof goal:

   937 	\begin{center}

   938 		$\blexer \; r \; s = \blexersimp \; r \; s$.

   939 	\end{center}