--- a/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Tue Jun 27 16:26:48 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded1.tex	Thu Jun 29 04:17:48 2023 +0100
@@ -9,9 +9,10 @@
 %its correctness proof in 
 %Chapter 3\ref{Chapter3}. 
 In this chapter, we are going to describe the bit-coded algorithm
-introduced by Sulzmann and Lu \parencite{Sulzmann2014} to address the growth problem of 
-derivatives of
-regular expressions. 
+introduced by Sulzmann and Lu \parencite{Sulzmann2014} and their correctness proof.
+%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