--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Tue Jun 27 01:09:36 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Tue Jun 27 16:26:48 2023 +0100
@@ -8,6 +8,10 @@
 %simplifications and therefore introduce our version of the bitcoded algorithm and 
 %its correctness proof in 
 %Chapter 3\ref{Chapter3}. 
+{\color{red} \rule{\linewidth}{0.5mm}}
+New content starts.
+{\color{red} \rule{\linewidth}{0.5mm}}
+
 \section{Overview}
 
 This chapter
@@ -100,31 +104,28 @@
 The $\blexer$ proof relies on a lockstep POSIX
 correspondence between the lexical value and the
 regular expression in each derivative and injection.
-If we zoom into the diagram \ref{fig:Inj} and look specifically at
-the pairs $v_i, r_i$ and $v_{i+1} r_{i+1}$, and the invariant of these
-pairs, we get the following correspondence 
+If we zoom into the diagram \ref{graph:in} and look specifically at
+the pairs $v_i, r_i$ and $v_{i+1},\, r_{i+1}$, we get the diagram demonstrating
+the invariant that the same bitcodes can be extracted from the pairs:
 
-\begin{tikzpicture}[
-  -{Stealth[scale=1.5]}, % arrow style
-  shorten >=1pt, % distance from node to arrow head
-  node distance=2cm,
-  font=\sffamily
-]
+When simplifications are added, the inhabitation relation no longer holds,
+causing the above diagram to break.
+
+Ausaf addressed this with an augmented lexer he called $\textit{slexer}$.
+
+
 
-\matrix (M) [matrix of nodes, nodes in empty cells, column sep=2cm, row sep=2cm,
-nodes={execute at begin node=\phantom}]
-{
-  1 & {$b_{s}(a_{0}+a_{1a})^{*}$} & 3 & 4\\
-  5 & 6 & 7 & 8\\
-  9 & 10 & 11 & 12\\
-};
+we note that the invariant
+$\vdash v_{i+1}: r_{i+1} \implies \retrieve \; r_{i+1} \; v_{i+1} $ is too strong
+to maintain because the precondition $\vdash v_i : r_i$ is too weak.
+It does not require $v_i$ to be a POSIX value 
+
 
-\foreach \i in {2,...,3} % go through each column
-  \draw[dotted] (M-1-\i) -- (M-2-\i) -- (M-3-\i);
+{\color{red} \rule{\linewidth}{0.5mm}}
+New content ends
+{\color{red} \rule{\linewidth}{0.5mm}}
 
-\foreach \i in {1,2} % go through each row
-  \draw[->] (M-\i-2.east) -- (M-\i-3.west);
-\end{tikzpicture}
+
 
 %
 %

--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Tue Jun 27 01:09:36 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Tue Jun 27 16:26:48 2023 +0100
@@ -616,6 +616,11 @@
 
 
 \section{Structure of the thesis}
+\marginpar{\em This is a marginal note.} 
+Before talking about the formal proof of $\blexersimp$'s 
+correctness, which is the main contribution of this thesis,
+we need to introduce two formal proofs which belong
+to Ausafe et al. 
 In chapter \ref{Inj} we will introduce the concepts
 and notations we 
 use for describing regular expressions and derivatives,