--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Mon Aug 29 23:16:28 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Tue Aug 30 12:41:52 2022 +0100
@@ -872,57 +872,71 @@
 The rewritability relation 
 $\rightsquigarrow$ is preserved under derivatives--
 it is just that we might need multiple steps 
-where originally only one step was needed.
+where originally only one step was needed:
 \begin{lemma}\label{rewriteBder}
-	$r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$ 
-	and
-	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies 
-	\map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$
-\end{lemma}
-\begin{proof}
-	By induction on $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.
-\end{proof}
-Now we can prove that once we could rewrite from one expression to another in many steps,
-then after a derivative on both sides we could still rewrite one to another in many steps:
-\begin{lemma}
-	$r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$
+	\hspace{0em}
+	\begin{itemize}
+		\item
+			If $r_1 \rightsquigarrow r_2$, then $r_1 \backslash c 
+			\rightsquigarrow^*  r_2 \backslash c$ 
+		\item	
+			If $rs_1 \stackrel{s}{\rightsquigarrow} rs_2$, then $ 
+			\map \; (\_\backslash c) \; rs_1 
+			\stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$
+	\end{itemize}
 \end{lemma}
 \begin{proof}
-	By rule induction of $\stackrel{*}{\rightsquigarrow} $ and using the previous lemma :\ref{rewriteBder}.
+	By induction on $\rightsquigarrow$ 
+	and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.
+\end{proof}
+\noindent
+Now we can prove property 3, as an immediate corollary:
+\begin{corollary}\label{rewritesBder}
+	$r_1 \rightsquigarrow^* r_2 \implies r_1 \backslash c \rightsquigarrow^*   
+	r_2 \backslash c$
+\end{corollary}
+\begin{proof}
+	By rule induction of $\stackrel{*}{\rightsquigarrow} $ and using the previous lemma \ref{rewriteBder}.
 \end{proof}
 \noindent
-This can be extended and combined with the previous two important properties
-so that a regular expression's successivve derivatives can be rewritten in many steps
-to its simplified counterpart:
+This can be extended and combined with $r \rightsquigarrow^* \textit{bsimp} \; r$
+to obtain the rewritability between
+$\blexer$ and $\blexersimp$'s intermediate
+derivative regular expressions 
 \begin{lemma}\label{bderBderssimp}
-	$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $
+	$a \backslash s \rightsquigarrow^* \bderssimp{a}{s} $
 \end{lemma}
+\begin{proof}
+	By an induction on $s$.
+\end{proof}
 \subsection{Main Theorem}
-Now with \ref{bdersBderssimp} we are ready for the main theorem.
-To link $\blexersimp$ and $\blexer$, 
-we first say that they give out the same bits, if the lexing result is a match:
-\begin{lemma}
-	$\bnullable \; (a \backslash s) \implies \bmkeps \; (a \backslash s) = \bmkeps \; (\bderssimp{a}{s})$
-\end{lemma}
-\noindent
-Now that they give out the same bits, we know that they give the same value after decoding,
-which we know is correct value as $\blexer$ is correct:
+Now with \ref{bderBderssimp} we are ready for the main theorem.
 \begin{theorem}
 	$\blexer \; r \; s = \blexersimp{r}{s}$
 \end{theorem}
 \noindent
 \begin{proof}
-	One can rewrite in many steps from the original lexer's derivative regular expressions to the 
-	lexer with simplification applied:
-	$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.
-	If two regular expressions are rewritable, then they produce the same bits.
-	Under the condition that $ r_1$ is nullable, we have
-	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$.
-	We have that 
-	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$ holds.
-	This proves the \emph{if}  branch of
-	$\blexer \; r \; s = \blexersimp{r}{s}$.
-
+	One can rewrite in many steps from the original lexer's 
+	derivative regular expressions to the 
+	lexer with simplification applied (by lemma \ref{bderBderssimp}):
+	\begin{center}
+		$a \backslash s \stackrel{*}{\rightsquigarrow} \bderssimp{a}{s} $.
+	\end{center}
+	we know that they give out the same bits, if the lexing result is a match:
+	\begin{center}
+		$\bnullable \; (a \backslash s) 
+		\implies \bmkeps \; (a \backslash s) = \bmkeps \; (\bderssimp{a}{s})$
+	\end{center}
+	Now that they give out the same bits, we know that they give the same value after decoding.
+	\begin{center}
+		$\bnullable \; (a \backslash s) 
+		\implies \decode \; r \; (\bmkeps \; (a \backslash s)) = 
+		\decode \; r \; (\bmkeps \; (\bderssimp{a}{s}))$
+	\end{center}
+	Which is equivalent to our proof goal:
+	\begin{center}
+		$\blexer \; r \; s = \blexersimp \; r \; s$.
+	\end{center}	
 \end{proof}
 \noindent
 As a corollary,