--- a/ChengsongTanPhdThesis/Chapters/ChapterBitcoded1.tex	Sat May 28 17:17:18 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/ChapterBitcoded1.tex	Mon May 30 14:41:09 2022 +0100
@@ -50,15 +50,87 @@
 
 
 
-
 %----------------------------------------------------------------------------------------
-%	SECTION corretness proof
+%	SECTION  correctness proof
 %----------------------------------------------------------------------------------------
-\section{Proof Technique of Correctness of Bit-coded Algorithm with Simplification}
-The non-trivial part of proving the correctness of the algorithm with simplification
-compared with not having simplification is that we can no longer use the argument 
-in \cref{flex_retrieve}.
-The function \retrieve needs the structure of the annotated regular expression to 
-agree with the structure of the value, but simplification will always mess with the 
-structure:
-%TODO: after simp does not agree with each other: (a + 0) --> a v.s. Left(Char(a))
\ No newline at end of file
+\section{Correctness of Bit-coded Algorithm (Without Simplification)}
+We now give the proof the correctness of the algorithm with bit-codes.
+
+Ausaf and Urban cleverly defined an auxiliary function called $\flex$,
+defined as
+\[
+\flex \; r \; f \; [] \; v \; = \; f\; v
+\flex \; r \; f \; c :: s \; v =  \flex r \; \lambda v. \, f (\inj \; r\; c\; v)\; s \; v
+\]
+which accumulates the characters that needs to be injected back, 
+and does the injection in a stack-like manner (last taken derivative first injected).
+$\flex$ is connected to the $\lexer$:
+\begin{lemma}
+$\flex \; r \; \textit{id}\; s \; \mkeps (r\backslash s) = \lexer \; r \; s$
+\end{lemma}
+$\flex$ provides us a bridge between $\lexer$ and $\blexer$.
+What is even better about $\flex$ is that it allows us to 
+directly operate on the value $\mkeps (r\backslash v)$,
+which is pivotal in the definition of  $\lexer $ and $\blexer$, but not visible as an argument.
+When the value created by $\mkeps$ becomes available, one can 
+prove some stepwise properties of lexing nicely:
+\begin{lemma}\label{flexStepwise}
+$\textit{flex} \; r \; f \; s@[c] \; v= \flex \; r \; f\; s \; (\inj \; (r\backslash s) \; c \; v) $
+\end{lemma}
+
+And for $\blexer$ we have a function with stepwise properties like $\flex$ as well,
+called $\retrieve$\ref{retrieveDef}.
+$\retrieve$ takes bit-codes from annotated regular expressions
+guided by a value.
+$\retrieve$ is connected to the $\blexer$ in the following way:
+\begin{lemma}\label{blexer_retrieve}
+$\blexer \; r \; s = \decode  \; (\retrieve \; (\internalise \; r) \; (\mkeps \; (r \backslash s) )) \; r$
+\end{lemma}
+If you take derivative of an annotated regular expression, 
+you can $\retrieve$ the same bit-codes as before the derivative took place,
+provided that you use the corresponding value:
+
+\begin{lemma}\label{retrieveStepwise}
+$\retrieve \; (r \backslash c)  \;  v= \retrieve \; r \; (\inj \; r\; c\; v)$
+\end{lemma}
+The other good thing about $\retrieve$ is that it can be connected to $\flex$:
+%centralLemma1
+\begin{lemma}\label{flex_retrieve}
+$\flex \; r \; \textit{id}\; s\; v = \decode \; (\retrieve \; (r\backslash s )\; v) \; r$
+\end{lemma}
+\begin{proof}
+By induction on $s$. The induction tactic is reverse induction on strings.
+$v$ is allowed to be arbitrary.
+The crucial point is to rewrite 
+\[
+\retrieve \; (r \backslash s@[c]) \; \mkeps (r \backslash s@[c]) 
+\]
+as
+\[
+\retrieve \; (r \backslash s) \; (\inj \; (r \backslash s) \; c\;  \mkeps (r \backslash s@[c]))
+\].
+This enables us to equate 
+\[
+\retrieve \; (r \backslash s@[c]) \; \mkeps (r \backslash s@[c]) 
+\] 
+with 
+\[
+\flex \; r \; \textit{id} \; s \; (\inj \; (r\backslash s) \; c\; (\mkeps (r\backslash s@[c])))
+\],
+which in turn can be rewritten as
+\[
+\flex \; r \; \textit{id} \; s@[c] \;  (\mkeps (r\backslash s@[c]))
+\].
+\end{proof}
+
+With the above lemma we can now link $\flex$ and $\blexer$.
+
+\begin{lemma}\label{flex_blexer}
+$\textit{flex} \; r \; \textit{id} \; s \; \mkeps(r \backslash s)  = \blexer \; r \; s$
+\end{lemma}
+\begin{proof}
+Using two of the above lemmas: \ref{flex_retrieve} and \ref{blexer_retrieve}.
+\end{proof}
+Finally 
+
+