--- a/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Sun May 08 13:26:31 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter2.tex	Sun May 08 15:29:17 2022 +0100
@@ -200,8 +200,28 @@
 bounds for future work.\\[-6.5mm]
 
 
+
+%-----------------------------------
+%	SECTION ?
+%-----------------------------------
+\section{preparatory properties for getting a finiteness bound}
+Before we get to the proof that says the intermediate result of our lexer will
+remain finitely bounded, which is an important efficiency/liveness guarantee,
+we shall first develop a few preparatory properties and definitions to 
+make the process of proving that a breeze.
+
+We define rewriting relations for $\rrexp$s, which allows us to do the 
+same trick as we did for the correctness proof,
+but this time we will have stronger equalities established.
+\subsection{"hrewrite" relation}
+List of simplifications for regular expressions simplification without bitcodes:
+\
+
+
+
+
 %----------------------------------------------------------------------------------------
-%	SECTION 2
+%	SECTION ??
 %----------------------------------------------------------------------------------------
 
 \section{"Closed Forms" of regular expressions' derivatives w.r.t strings}