diff -r a365d1364640 -r deb35fd780fe ChengsongTanPhdThesis/Chapters/Bitcoded2.tex
--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Wed Jun 21 22:43:04 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Tue Jun 27 01:09:36 2023 +0100
@@ -81,25 +81,58 @@
 in the inhabitation relation, something different than $v_{r}^{c}$ needs to be plugged
 in for the above statement to hold.
 Ausaf et al. \cite{AusafUrbanDyckhoff2016}
-made some initial attempts on the un-annotated lexer (to be continued)
+made some initial attempts with this idea, see \cite{FahadThesis}
+for details.
+The other route is to dispose of lemma \ref{retrieveStepwise},
+and prove a slightly weakened inductive invariant instead.
+We adopt this approach in this thesis.
 
-
+We first introduce why the inductive invariant in $\blexer$'s proof
+is too strong, and suggest a few possible fixes, which leads to
+our proof which we believe was the most natural and effective method.
 
 
 
-From this chapter we start with the main contribution of this thesis, which
+\section{Why Lemma \ref{retrieveStepwise}'s Requirement is too Strong}
 
-o
-In particular, the $\blexer$ proof relies on a lockstep POSIX
+%From this chapter we start with the main contribution of this thesis, which
+
+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 
 
+\begin{tikzpicture}[
+  -{Stealth[scale=1.5]}, % arrow style
+  shorten >=1pt, % distance from node to arrow head
+  node distance=2cm,
+  font=\sffamily
+]
 
-which is essential for getting an understanding this thesis
-in chapter \ref{Bitcoded1}, which is necessary for understanding why
-the proof 
+\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\\
+};
+
+\foreach \i in {2,...,3} % go through each column
+  \draw[dotted] (M-1-\i) -- (M-2-\i) -- (M-3-\i);
 
-In this chapter,
+\foreach \i in {1,2} % go through each row
+  \draw[->] (M-\i-2.east) -- (M-\i-3.west);
+\end{tikzpicture}
+
+%
+%
+%which is essential for getting an understanding this thesis
+%in chapter \ref{Bitcoded1}, which is necessary for understanding why
+%the proof 
+%
+%In this chapter,
 
 %We contrast our simplification function 
 %with Sulzmann and Lu's, indicating the simplicity of our algorithm.