diff -r c334f0b3ef52 -r cc54ce075db5 ChengsongTanPhdThesis/Chapters/Bitcoded2.tex
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Fri Jun 03 16:45:30 2022 +0100
@@ -0,0 +1,64 @@
+% Chapter Template
+
+% Main chapter title
+\chapter{Correctness of Bit-coded Algorithm with Simplification}
+
+\label{Bitcoded2} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}
+%Then we illustrate how the algorithm without bitcodes falls short for such aggressive 
+%simplifications and therefore introduce our version of the bitcoded algorithm and 
+%its correctness proof in 
+%Chapter 3\ref{Chapter3}. 
+
+
+
+
+%----------------------------------------------------------------------------------------
+%	SECTION common identities
+%----------------------------------------------------------------------------------------
+\section{Common Identities In Simplification-Related Functions} 
+Need to prove these before starting on the big correctness proof.
+
+%-----------------------------------
+%	SUBSECTION 
+%-----------------------------------
+\subsection{Idempotency of $\simp$}
+
+\begin{equation}
+	\simp \;r = \simp\; \simp \; r 
+\end{equation}
+This property means we do not have to repeatedly
+apply simplification in each step, which justifies
+our definition of $\blexersimp$.
+It will also be useful in future proofs where properties such as 
+closed forms are needed.
+The proof is by structural induction on $r$.
+
+%-----------------------------------
+%	SUBSECTION 
+%-----------------------------------
+\subsection{Syntactic Equivalence Under $\simp$}
+We prove that minor differences can be annhilated
+by $\simp$.
+For example,
+\begin{center}
+$\simp \;(\simpALTs\; (\map \;(\_\backslash \; x)\; (\distinct \; \mathit{rs}\; \phi))) = 
+ \simp \;(\simpALTs \;(\distinct \;(\map \;(\_ \backslash\; x) \; \mathit{rs}) \; \phi))$
+\end{center}
+
+
+
+
+
+
+
+%----------------------------------------------------------------------------------------
+%	SECTION corretness 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