--- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Tue Aug 02 22:11:22 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Fri Aug 12 00:39:23 2022 +0100
@@ -760,6 +760,17 @@
 	Straightforward corollary of \ref{flex_blexer}.
 \end{proof}
 \noindent
+To piece things together and spell out the exact correctness
+of the bitcoded lexer
+in terms of producing POSIX values,
+we use the fact from the previous chapter that
+\[
+	If \; (r, s) \rightarrow v \; then \; \lexer \; r \; s = v
+\]
+to obtain this corollary:
+\begin{corollary}\label{blexerPOSIX}
+	$If \; (r, s) \rightarrow v \; then \blexer \; r \; s = v$
+\end{corollary}
 Our main reason for wanting a bit-coded algorithm over 
 the injection-based one is for its capabilities of allowing
 more aggressive simplifications.