--- a/ChengsongTanPhdThesis/Chapters/Chapter3.tex	Thu May 26 20:51:40 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Chapter3.tex	Fri May 27 18:27:39 2022 +0100
@@ -1,16 +1,26 @@
 % Chapter Template
 
-\chapter{Common Identities In Simplification-Related Functions} % Main chapter title
+% Main chapter title
 
-\label{ChapterX} % Change X to a consecutive number; for referencing this chapter elsewhere, use \ref{ChapterX}
+\label{Chapter3} % 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 1
+%	SECTION common identities
 %----------------------------------------------------------------------------------------
+\section{Common Identities In Simplification-Related Functions} 
+Need to prove these before starting on the big correctness proof.
 
-\section{Idempotency of $\simp$}
+%-----------------------------------
+%	SUBSECTION 
+%-----------------------------------
+\subsection{Idempotency of $\simp$}
 
 \begin{equation}
 	\simp \;r = \simp\; \simp \; r 
@@ -23,7 +33,7 @@
 The proof is by structural induction on $r$.
 
 %-----------------------------------
-%	SUBSECTION 1
+%	SUBSECTION 
 %-----------------------------------
 \subsection{Syntactic Equivalence Under $\simp$}
 We prove that minor differences can be annhilated
@@ -35,17 +45,19 @@
 \end{center}
 
 
-%-----------------------------------
-%	SUBSECTION 2
-%-----------------------------------
+
 
-\subsection{Subsection 2}
-Morbi rutrum odio eget arcu adipiscing sodales. Aenean et purus a est pulvinar pellentesque. Cras in elit neque, quis varius elit. Phasellus fringilla, nibh eu tempus venenatis, dolor elit posuere quam, quis adipiscing urna leo nec orci. Sed nec nulla auctor odio aliquet consequat. Ut nec nulla in ante ullamcorper aliquam at sed dolor. Phasellus fermentum magna in augue gravida cursus. Cras sed pretium lorem. Pellentesque eget ornare odio. Proin accumsan, massa viverra cursus pharetra, ipsum nisi lobortis velit, a malesuada dolor lorem eu neque.
+
+
 
 %----------------------------------------------------------------------------------------
-%	SECTION 2
+%	SECTION corretness proof
 %----------------------------------------------------------------------------------------
-
-\section{Main Section 2}
-
-Sed ullamcorper quam eu nisl interdum at interdum enim egestas. Aliquam placerat justo sed lectus lobortis ut porta nisl porttitor. Vestibulum mi dolor, lacinia molestie gravida at, tempus vitae ligula. Donec eget quam sapien, in viverra eros. Donec pellentesque justo a massa fringilla non vestibulum metus vestibulum. Vestibulum in orci quis felis tempor lacinia. Vivamus ornare ultrices facilisis. Ut hendrerit volutpat vulputate. Morbi condimentum venenatis augue, id porta ipsum vulputate in. Curabitur luctus tempus justo. Vestibulum risus lectus, adipiscing nec condimentum quis, condimentum nec nisl. Aliquam dictum sagittis velit sed iaculis. Morbi tristique augue sit amet nulla pulvinar id facilisis ligula mollis. Nam elit libero, tincidunt ut aliquam at, molestie in quam. Aenean rhoncus vehicula hendrerit.
+\section{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