--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Thu Jun 29 04:17:48 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Fri Jul 07 20:03:05 2023 +0100
@@ -20,22 +20,23 @@
 in detail. 
 The material in the
 previous
-chapters is necessary 
-material for setting the scene of the formal proof we
-are about to describe.
-
-The fundamental reason is we cannot extend the correctness proof of theorem 4,
+chapters is necessary for this thesis,
+because it provides the context for why we need a new framework for
+the proof of $\blexersimp$.
+%material for setting the scene of the formal proof we
+%are about to describe.
+The fundamental reason is we cannot extend the correctness proof of theorem 4
 because lemma 13 does not hold anymore when simplifications are involved.
-
-The proof details are necessary materials for this thesis
-because it provides necessary context to explain why we need a
-new framework for the proof of $\blexersimp$, which involves
-simplifications that cause structural changes to the regular expression.
-A new formal proof of the correctness of $\blexersimp$, where the 
-proof of $\blexer$
-is not applicatble in the sense that we cannot straightforwardly extend the
-proof of theorem \ref{blexerCorrect} because lemma \ref{retrieveStepwise} does
-not hold anymore.
+\marginpar{\em rephrased things so they make better sense.}
+%The proof details are necessary materials for this thesis
+%because it provides necessary context to explain why we need a
+%new framework for the proof of $\blexersimp$, which involves
+%simplifications that cause structural changes to the regular expression.
+%A new formal proof of the correctness of $\blexersimp$, where the 
+%proof of $\blexer$
+%is not applicatble in the sense that we cannot straightforwardly extend the
+%proof of theorem \ref{blexerCorrect} because lemma \ref{retrieveStepwise} does
+%not hold anymore.
 %This is because the structural induction on the stepwise correctness
 %of $\inj$ breaks due to each pair of $r_i$ and $v_i$ described
 %in chapter \ref{Inj} and \ref{Bitcoded1} no longer correspond to
@@ -53,11 +54,13 @@
 chapter \ref{Bitcoded1} formalised by Ausaf et al.
 relies crucially on lemma \ref{retrieveStepwise} that says
 any value can be retrieved in a stepwise manner, namely:
-\begin{center}%eqref: this proposition needs to be referred	
-	$\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c)  \;  v= \retrieve \; r \; (\inj \; r\; c\; v)$
-\end{center}
-This no longer holds once we introduce simplifications.
-Simplifications are necessary to control the size of derivatives 
+\begin{equation}\label{eq:stepwise}%eqref: this proposition needs to be referred	
+	\vdash v : (r\backslash c) \implies \retrieve \; (r \backslash c)  \;  v= \retrieve \; r \; (\inj \; r\; c\; v)
+\end{equation}
+%This no longer holds once we introduce simplifications.
+Simplifications are necessary to control the size of derivatives,
+but they also destroy the structures of the regular expressions
+such that \ref{eq:stepwise} does not hold.
 
 
 We want to prove the correctness of $\blexersimp$ which integrates

--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Thu Jun 29 04:17:48 2023 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Fri Jul 07 20:03:05 2023 +0100
@@ -204,7 +204,7 @@
 
 %TODO: look up snort rules to use here--give readers idea of what regexes look like
 
-
+\marginpar{rephrasing using "imprecise words"}
 Regular expressions, since their inception in the 1940s, 
 have been subject to extensive study and implementation. 
 Their primary application lies in text processing--finding
@@ -215,12 +215,11 @@
 to recognise email addresses is
 \marginpar{rephrased from "the regex for recognising" to "a simple regex that tries to match email"}
 \begin{center}
-$[a-z0-9.\_]^\backslash+@[a-z0-9.-]^\backslash+\.\{a-z\}\{2,6\}$
+\verb|[a-z0-9._]^+@[a-z0-9.-]^+\.\{a-z\}\{2,6\}|
 %$[a-z0-9._]^+@[a-z0-9.-]^+\.[a-z]{2,6}$.
 \end{center}
 \marginpar{Simplified example, but the distinction between . and escaped . is correct
-and therefore left unchanged.}
-
+and therefore left unchanged. Also verbatim package does not straightforwardly support superscripts so + kept as they are.}
 %Using this, regular expression matchers and lexers are able to extract 
 %the domain names by the use of \verb|[a-zA-Z0-9.-]+|. 
 \marginpar{Rewrote explanation for the expression.}