diff -r 3cbcd7cda0a9 -r 0497408a3598 ChengsongTanPhdThesis/Chapters/ChapterBitcoded2.tex
--- a/ChengsongTanPhdThesis/Chapters/ChapterBitcoded2.tex	Wed Jul 13 08:27:28 2022 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-% Chapter Template
-
-% Main chapter title
-\chapter{Correctness of Bit-coded Algorithm with Simplification}
-
-\label{ChapterBitcoded2} % 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