% Chapter Template

% Main chapter title
\chapter{Correctness of Bit-coded Algorithm without Simplification}

\label{ChapterBitcoded1} % 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))