--- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Fri May 26 23:42:15 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Sun Jun 18 17:54:52 2023 +0100
@@ -1235,6 +1235,12 @@
 	is function $\erase$'s cases.
 \end{proof}
 \noindent
+Intuitively the lemma can be understood as all lexical value
+information being preserved and recoverable throughout each lexing step.
+We shall see in the next chapter that this no longer
+holds with simplifications which takes away certain sub-expressions
+corresponding to non-POSIX lexical values.
+
 Before we move on to the next
 helper function, we rewrite $\blexer$ in
 the following way which makes later proofs more convenient:
@@ -1340,7 +1346,7 @@
 \noindent
 With this pivotal lemma we can now link $\flex$ and $\blexer$
 and finally give the correctness of $\blexer$--it outputs the same result as $\lexer$:
-\begin{theorem}
+\begin{theorem}\label{blexerCorrect}
 	$\blexer\; r \; s = \lexer \; r \; s$
 \end{theorem}
 \begin{proof}