--- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Mon Jul 24 11:09:48 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Tue Jul 25 17:28:29 2023 +0100
@@ -10,14 +10,30 @@
 %Chapter 3\ref{Chapter3}. 
 In this chapter, we are going to describe the bit-coded algorithm
 introduced by Sulzmann and Lu \parencite{Sulzmann2014} and their correctness proof.
+Just like in chapter \ref{Inj}, the algorithms and proofs have been included
+for self-containedness reasons,
+even though they have been originally found and described by
+Sulzmann and Lu (\cite{Sulzmann2014}) and 
+Ausaf et al. (\cite{AusafDyckhoffUrban2016} and \cite{Ausaf}).
+%In addition to this, the 
+The details of the proofs in this thesis 
+also follow more closely the actual Isabelle formalisation.
+For example, lemma \ref{flexStepwise} and \ref{retrieveStepwise}
+are not included in the publications by Ausaf et al., despite them being
+some of the key lemmas leading to the correctness result.
+
+We will first motivate the bit-coded algorithm in section \ref{bitMotivate},
+and then introduce their formal definitions in section \ref{bitDef},
+followed by a description of the correctness proof of $\blexer$ in section \ref{blexerProof}.
+
 %to address the growth problem of 
 %derivatives of
 %regular expressions. 
-We have implemented their algorithm in Scala and Isabelle, 
-and found problems 
-in their algorithm, such as de-duplication not working properly and redundant
-fixpoint construction. 
-\section{The Motivation Behind Using Bitcodes}
+%We have implemented their algorithm in Scala and Isabelle, 
+%and found problems 
+%in their algorithm, such as de-duplication not working properly and redundant
+%fixpoint construction. 
+\section{The Motivation Behind Using Bitcodes}\label{bitMotivate}
 Let us give again the definition of $\lexer$ from Chapter \ref{Inj}:
 \begin{center}
 \begin{tabular}{lcl}
@@ -316,7 +332,7 @@
 The stack seems to grow at least quadratically with respect
 to the input (not taking into account the size bloat of $r_i$),
 which can be inefficient and prone to stack overflows.
-\section{Bitcoded Algorithm}
+\section{Bitcoded Algorithm}\label{bitDef}
 To address this,
 Sulzmann and Lu defined a new datatype 
 called \emph{annotated regular expression},
@@ -1042,7 +1058,7 @@
 %-----------------------------------
 %	SUBSECTION 1
 %-----------------------------------
-\section{Correctness Proof of $\textit{Blexer}$}
+\section{Correctness Proof of $\textit{Blexer}$}\label{blexerProof}
 Why is $\blexer$ correct?
 In other words, why is it the case that 
 $\blexer$ outputs the same value as $\lexer$?