diff -r 753a3b0ee02b -r 00171b627b8d ChengsongTanPhdThesis/Chapters/Bitcoded1.tex
--- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Sat Jul 08 22:18:22 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Sun Jul 09 00:29:02 2023 +0100
@@ -1181,7 +1181,23 @@
 final derivative $a_n$, guided by $v_n$. This can be proved
 as follows:
 \begin{lemma}\label{bmkepsRetrieve}
-	$\bnullable \; a \implies \bmkeps \; a = \retrieve \; a \; (\mkeps \; (\erase \; a))$
+	\mbox{}
+	\begin{itemize}
+		\item
+If $\forall v \in vs. \vdash v : r$, and  $\code \; v = \retrieve \; (\internalise\; r) \; v$\\
+then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \;  r)^*) \; (\Stars \; vs)$
+		\item
+	$\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
+		\item
+	$\bnullable \; a \implies \bmkeps \; a = \retrieve \; a \; (\mkeps \; (a_\downarrow))$
+	\end{itemize}
+\begin{proof}
+	The first part is by induction on the value list $vs$.
+	The second part is by induction on $r$,
+	and the star case uses the first part.
+	The last part is by a routine induction on $a$.
+\end{proof}
+\noindent
 \end{lemma}
 \begin{proof}
 	By a routine induction on $a$.
@@ -1190,34 +1206,34 @@
 %The design of $\retrieve$ enables us to extract bitcodes
 %from both annotated regular expressions and values.
 %$\retrieve$ always ``sucks up'' all the information.
-When more information is stored in the value, we would be able to
-extract more from the value, and vice versa.
-For example in star iterations, $\retrieve$ will be able to extract from $\Stars \; vs$
-exactly the same bitcodes as $\code \; (\Stars \; vs)$:
-\begin{lemma}\label{retrieveEncodeSTARS}
-  If $\forall v \in vs. \vdash v : r$, and  $\code \; v = \retrieve \; (\internalise\; r) \; v$\\
-  then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \;  r)^*) \; (\Stars \; vs)$
-\end{lemma}
-\begin{proof}
-	By induction on the value list $vs$.
-\end{proof}
-\noindent
-Similarly, when the value list does not hold information,
-only the bitcodes plus some delimiter will be recorded:
-\begin{center}
-  $\retrieve \; _{bs}((\internalise \;  r)^*) \; (\Stars \; [] )  = bs @ [S]$.
-\end{center}
-In general, if we have a regular expression that is just internalised
-and the final lexing result value, we can $\retrieve$ the bitcodes
-that look as if we have en$\code$-ed the value as bitcodes:
-\begin{lemma}
-	$\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
-\end{lemma}
-\begin{proof}
-	By induction on $r$.
-	The star case uses lemma \ref{retrieveEncodeSTARS}.
-\end{proof}
-\noindent
+%When more information is stored in the value, we would be able to
+%extract more from the value, and vice versa.
+%For example in star iterations, $\retrieve$ will be able to extract from $\Stars \; vs$
+%exactly the same bitcodes as $\code \; (\Stars \; vs)$:
+%\begin{lemma}\label{retrieveEncodeSTARS}
+%  If $\forall v \in vs. \vdash v : r$, and  $\code \; v = \retrieve \; (\internalise\; r) \; v$\\
+%  then $\code \; (\Stars \; vs) = \retrieve \; _{[]}((\internalise \;  r)^*) \; (\Stars \; vs)$
+%\end{lemma}
+%\begin{proof}
+%	By induction on the value list $vs$.
+%\end{proof}
+%\noindent
+%Similarly, when the value list does not hold information,
+%only the bitcodes plus some delimiter will be recorded:
+%\begin{center}
+%  $\retrieve \; _{bs}((\internalise \;  r)^*) \; (\Stars \; [] )  = bs @ [S]$.
+%\end{center}
+%In general, if we have a regular expression that is just internalised
+%and the final lexing result value, we can $\retrieve$ the bitcodes
+%that look as if we have en$\code$-ed the value as bitcodes:
+%\begin{lemma}
+%	$\vdash v : r \implies \retrieve \; (r)^\uparrow \; v = \code \; v$
+%\end{lemma}
+%\begin{proof}
+%	By induction on $r$.
+%	The star case uses lemma \ref{retrieveEncodeSTARS}.
+%\end{proof}
+%\noindent
 The following property of $\retrieve$ is crucial, as
 it provides a "bridge" between $a_0$ and $a_n $ in the
 lexing diagram by linking adjacent regular expressions $a_i$ and
@@ -1228,7 +1244,8 @@
 before the derivative took place,
 provided that the corresponding values are used respectively:
 \begin{lemma}\label{retrieveStepwise}
-	$\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c)  \;  v= \retrieve \; r \; (\inj \; r\; c\; v)$
+	$\vdash v : (a\backslash c)_\downarrow \implies \retrieve \; (a \backslash c)  \;  v= 
+							\retrieve \; a \; (\inj \; a_\downarrow\; c\; v)$
 \end{lemma}
 \begin{proof}
 	We do an induction on $r$, generalising over $v$.
@@ -1242,16 +1259,16 @@
 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:
-\begin{lemma}\label{blexer_retrieve}
-$\blexer \; r \; s = \decode  \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$
-\end{lemma}
-\begin{proof}
-	Using lemma \ref{bmkepsRetrieve}.
-\end{proof}
-\noindent
+%Before we move on to the next
+%helper function, we rewrite $\blexer$ in
+%the following way which makes later proofs more convenient:
+%\begin{lemma}\label{blexer_retrieve}
+%$\blexer \; r \; s = \decode  \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$
+%\end{lemma}
+%\begin{proof}
+%	Using lemma \ref{bmkepsRetrieve}.
+%\end{proof}
+%\noindent
 The function $\retrieve$ allows connecting
 between the intermediate 
 results $a_i$ and $a_{i+1}$ in $\blexer$.
@@ -1351,13 +1368,25 @@
 	$\blexer\; r \; s = \lexer \; r \; s$
 \end{theorem}
 \begin{proof}
-	From \ref{flex_retrieve} we have that 
-	$\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s)  = \blexer \; r \; s$,
-	which immediately implies this theorem.
+	We can rewrite the expression $\blexer \; r \; s$ by using lemma \ref{bmkepsRetrieve}:
+\[
+	\blexer \; r \; s = \decode  \; (\retrieve \; (\; r^\uparrow) \; (\mkeps \; (r \backslash s) )) \; r
+\]
+	From \ref{flex_retrieve} we have that the left-hand-side is equal to 
+\[
+	\textit{flex} \; r \; \textit{id} \; s \; \mkeps \; (r \backslash s),
+\]
+which in turn equals 
+\[
+	\lexer \; r \; s.
+\]
+	%which immediately implies this theorem.
 \end{proof}
 \noindent
-To piece things together and spell out the correctness
-result of the bitcoded lexer more explicitly,
+To piece things together 
+%and spell out the correctness
+%result of the bitcoded lexer more explicitly,
+and give the correctness result explicitly,
 we use the fact from the previous chapter that
 \[
 	 (r, s) \rightarrow v \;\; \textit{iff} \;\; \lexer \; r \; s =\Some \;  v
@@ -1366,9 +1395,13 @@
 \]
 to obtain this corollary:
 \begin{corollary}\label{blexerPOSIX}
-	The $\blexer$ function correctly implements a POSIX lexer, namely\\
-	$(r, s) \rightarrow v \;\; \textit{iff} \;\; \blexer \; r \; s = \Some \; v$\\
+	The $\blexer$ function correctly implements a POSIX lexer, namely
+	\begin{itemize}
+	\item
+	$(r, s) \rightarrow v \;\; \textit{iff} \;\; \blexer \; r \; s = \Some \; v$
+	\item
 	$\nexists v. (r, s) \rightarrow v\;\; \textit{iff} \;\; \blexer \;r\;s = None$
+	\end{itemize}
 \end{corollary}
 Our main reason for analysing the bit-coded algorithm over 
 the injection-based one is that it allows us to define