--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Tue Aug 02 22:11:22 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Fri Aug 12 00:39:23 2022 +0100
@@ -219,10 +219,26 @@
 %	SECTION rewrite relation
 %----------------------------------------------------------------------------------------
 \section{The Rewriting Relation $\rrewrite$($\rightsquigarrow$)}
-The overall idea for the correctness 
-\begin{conjecture}
-	$\blexersimp \; r \; s = \blexer \; r\; s$
-\end{conjecture}
+In the $\blexer$'s correctness proof, we
+did not directly derive the fact that $\blexer$ gives out the POSIX value,
+but first prove that $\blexer$ is linked with $\lexer$.
+Then we re-use
+the correctness of $\lexer$.
+Here we follow suit by first proving that
+$\blexersimp \; r \; s $ 
+produces the same output as $\blexer \; r\; s$,
+and then putting it together with 
+$\blexer$'s correctness result
+($(r, s) \rightarrow v \implies \blexer \; r \;s = v$)
+to obtain half of the correctness property (the other half
+being when $s$ is not $L \; r$ which is routine to establish)
+\begin{center}
+	$(r, s) \rightarrow v \implies \blexersimp \; r \; s = v$
+\end{center}
+\noindent
+because it makes the proof simpler
+The overall idea for the correctness of our simplified bitcoded lexer
+\noindent
 is that the $\textit{bsimp}$ will not change the regular expressions so much that
 it becomes impossible to extract the $\POSIX$ values.
 To capture this "similarity" between unsimplified regular expressions and simplified ones,
@@ -456,7 +472,7 @@
 have two regular expressions, one rewritable in many steps to the other,
 and one of them is $\bnullable$, then they will both yield the same bits under $\bmkeps$:
 \begin{lemma}
-	$(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) \implies \bmkeps \; r = \bmkeps \; r'$
+	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r' \;\; \text{and} \;\; \bnullable \; r_1 \;\; \text{then} \;\; \bmkeps \; r = \bmkeps \; r'$
 \end{lemma}
 \begin{proof}
 	By rule induction of $\stackrel{*}{\rightsquigarrow} $, using \ref{rewriteBmkepsAux} and $\ref{rewritesBnullable}$.
@@ -516,6 +532,28 @@
 	$\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'$.
+	This proves the \emph{if} (interesting) branch of
+	$\blexer \; r \; s = \blexersimp{r}{s}$.
+
+\end{proof}
+\noindent
+As a corollary,
+we link this result with the lemma we proved earlier that 
+\begin{center}
+	$(r, s) \rightarrow v \implies \blexer \; r \; s = v$
+\end{center}
+and obtain the corollary that the bit-coded lexer with simplification is
+indeed correctly outputting POSIX lexing result, if such a result exists.
+\begin{corollary}
+	$(r, s) \rightarrow v \implies \blexersimp{r}{s}$
+\end{corollary}
 
 \subsection{Comments on the Proof Techniques Used}
 The non-trivial part of proving the correctness of the algorithm with simplification