# HG changeset patch
# User Chengsong
# Date 1661767006 -3600
# Node ID 826af400b0686a2c8281d621fe90ab3cadae24fe
# Parent  4969ef817d929b4833811bff4e514190ca1833e6
more chap4

diff -r 4969ef817d92 -r 826af400b068 ChengsongTanPhdThesis/Chapters/Bitcoded2.tex
--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Sat Aug 27 00:37:03 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Mon Aug 29 10:56:46 2022 +0100
@@ -613,25 +613,54 @@
 gave in the previous section 
 have their ``many-steps version'':
 
-\begin{lemma}
+\begin{lemma}\label{squig1}
 	\hspace{0em}
 	\begin{itemize}
 		\item
 			$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies _{bs} \sum rs_1 \stackrel{*}{\rightsquigarrow} _{bs} \sum rs_2$
 		\item
-			$r \stackrel{*}{\rightsquigarrow} r' \implies _{bs} \sum r :: rs \stackrel{*}{\rightsquigarrow}  _{bs} \sum r' :: rs$
+			$r \rightsquigarrow^* r' \implies _{bs} \sum (r :: rs)\; \rightsquigarrow^*\;  _{bs} \sum (r' :: rs)$
+
+		\item
+			The rewriting in many steps property is composible 
+			in terms of the sequence constructor:\\
+			$r_1 \rightsquigarrow^* r_2 
+			\implies _{bs} r_1 \cdot r_3 \rightsquigarrow^* \;  
+			_{bs} r_2 \cdot r_3 \quad $ 
+			and 
+			$\quad r_3 \rightsquigarrow^* r_4 
+			\implies _{bs} r_1 \cdot r_3 \rightsquigarrow^* _{bs} \; r_1 \cdot r_4$
+		\item
+			The rewriting in many steps properties 
+			$\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ 
+			is preserved under the function $\fuse$:\\
+				$r_1 \rightsquigarrow^* r_2 
+				\implies \fuse \; bs \; r_1 \rightsquigarrow^* \; 
+				\fuse \; bs \; r_2 \quad  $ and 
+				$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 
+				\implies \map \; (\fuse \; bs) \; rs_1 
+				\stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs) \; rs_2$
 	\end{itemize}
 \end{lemma}
 \begin{proof}
 	By an induction on 
 	the inductive cases of $\stackrel{s*}{\rightsquigarrow}$ and $\rightsquigarrow^*$ respectively.
+	The third and fourth points are 
+	by the properties $r_1 \rightsquigarrow r_2 \implies \fuse \; bs \; r_1 \implies \fuse \; bs \; r_2$ and
+	$rs_2 \stackrel{s}{\rightsquigarrow} rs_3 
+	\implies \map \; (\fuse \; bs) rs_2 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs)\; rs_3$,
+	which can be indutively proven by the inductive cases of $\rightsquigarrow$ and 
+	$\stackrel{s}{\rightsquigarrow}$.
 \end{proof}
 \noindent
 The inference rules of $\stackrel{s}{\rightsquigarrow}$
 are defined in terms of list cons operation, here
 we establish that the 
 $\stackrel{s}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ 
-relation is also preserved w.r.t appending and prepending of a list:
+relation is also preserved w.r.t appending and prepending of a list.
+In addition, we
+also prove some relations 
+between $\rightsquigarrow^*$ and $\stackrel{s*}{\rightsquigarrow}$.
 \begin{lemma}\label{ssgqTossgs}
 	\hspace{0em}
 	\begin{itemize}
@@ -640,12 +669,28 @@
 
 		\item
 			$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies 
-			rs @ rs_1 \stackrel{s*}{\rightsquigarrow} rs @ rs_2$
+			rs @ rs_1 \stackrel{s*}{\rightsquigarrow} rs @ rs_2 \; \;
+			\textit{and} \; \;
+			rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
+			
 		\item
 			The $\stackrel{s}{\rightsquigarrow} $ relation after appending 
 			a list becomes $\stackrel{s*}{\rightsquigarrow}$:\\
-			$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
-
+			$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 
+			\implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
+		\item
+		
+			$r_1 \rightsquigarrow^* r_2 \implies [r_1] \stackrel{s*}{\rightsquigarrow} [r_2]$
+		\item
+		
+			$rs_3 \stackrel{s*}{\rightsquigarrow} rs_4 \land r_1 \rightsquigarrow^* r_2 \implies
+			r_2 :: rs_3 \stackrel{s*}{\rightsquigarrow} r_2 :: rs_4$
+		\item			
+			If we could rewrite a regular expression 
+			in many steps to $\ZERO$, then 
+			we could also rewrite any sequence containing it to $\ZERO$:\\
+			$r_1 \rightsquigarrow^* \ZERO 
+			\implies _{bs}r_1\cdot r_2 \rightsquigarrow^* \ZERO$
 	\end{itemize}
 \end{lemma}
 \begin{proof}
@@ -653,181 +698,186 @@
 	The second part is by induction on the inductive cases of $\stackrel{s*}{\rightsquigarrow}$.
 	The third part is 
 	by rule induction of $\stackrel{s}{\rightsquigarrow}$.
-\end{proof}
-\begin{lemma}
-	$rs_1 \stackrel{s*}{\rightsquigarrow} rs_2 \implies rs_1 @ rs \stackrel{s*}{\rightsquigarrow} rs_2 @ rs$
-\end{lemma}
-\begin{proof}
-	By rule induction of $\stackrel{s*}{\rightsquigarrow}$ and using \ref{ssgqTossgs}.
+	The fourth sub-lemma is 
+	by rule induction of 
+	$\stackrel{s*}{\rightsquigarrow}$ and using part one to three. 
+	The fifth part is a corollary of part four.
+	The last part is proven by rule induction again on $\rightsquigarrow^*$.
 \end{proof}
-Here are two lemmas relating $\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$:
-\begin{lemma}\label{singleton}
-	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies [r_1] \stackrel{s*}{\rightsquigarrow} [r_2]$
-\end{lemma}
-\begin{proof}
-	By rule induction of $ \stackrel{*}{\rightsquigarrow} $.
-\end{proof}
-\begin{lemma}
-	$rs_3 \stackrel{s*}{\rightsquigarrow} rs_4 \land r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies
-	r_2 :: rs_3 \stackrel{s*}{\rightsquigarrow} r_2 :: rs_4$
-\end{lemma}
-\begin{proof}
-	By using \ref{singleton}.
-\end{proof}
-In this section we give details for the proofs of the below properties:
+\noindent
+Now we are ready to give the proofs of the below properties:
 \begin{itemize}
 	\item
-		$(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) 
+		$(r \rightsquigarrow^* r'\land \bnullable \; r_1) 
 		\implies \bmkeps \; r = \bmkeps \; r'$. \\
-		If we can rewrite 
-		in many steps from $r$ to $r'$, then they  
-		will produce the same bitcodes 
-		under $\bmkeps$. 
 	\item
 		$r \rightsquigarrow^* \textit{bsimp} \;r$.\\
-		The simplification function
-		$\textit{bsimp}$ only transforms the regex $r$ using steps specified by 
-		$\rightsquigarrow^*$ and nothing else.
 	\item
 		$r \rightsquigarrow r' \implies r \backslash c \rightsquigarrow^* r'\backslash c$.\\
-		The rewritability relation $\rightsquigarrow$ is preserved under derivatives--
-		it is just that we might need more steps.
 \end{itemize}
 These properties would work together towards the correctness theorem.
-We start proving each of these lemmas below.
-\subsubsection{Property 1: $(r \stackrel{*}{\rightsquigarrow} r'\land \bnullable \; r_1) \implies \bmkeps \; r = \bmkeps \; r'$}
-Intuitively this property says we can 
-extract the same bitcodes from the nullable
-components of two regular expressions
-if we can rewrite from one to the other.
-
-
+\subsubsection{Property 1: $(r \rightsquigarrow^* r'\land \bnullable \; r_1) 
+		\implies \bmkeps \; r = \bmkeps \; r'$}
+Intuitively, this property says we can 
+extract the same bitcodes using $\bmkeps$ from the nullable
+components of two regular expressions $r$ and $r'$,
+if we can rewrite from one to the other in finitely
+many steps.\\
+For convenience, 
+we define a predicate for a list of regular expressions
+having at least one nullable regular expressions:
+\begin{center}
+	$\textit{bnullables} \; rs \quad \dn \quad \exists r \in rs. \;\; \bnullable \; r$
+\end{center}
+\noindent
+The rewriting relation $\rightsquigarrow$ preserves nullability:
+\begin{lemma}\label{rewritesBnullable}
+	\hspace{0em}
+	\begin{itemize}
+		\item
+			$\text{If} \; r_1 \rightsquigarrow r_2, \; 
+			\text{then} \; \bnullable \; r_1 = \bnullable \; r_2$
+		\item 	
+			$\text{If} \; rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \;
+			\text{then} \; \textit{bnullables} \; rs_1 = \textit{bnullables} \; rs_2$
+		\item
+			$r_1 \rightsquigarrow^* r_2 
+			\implies \bnullable \; r_1 = \bnullable \; r_2$
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	By rule induction of $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$.
+	The third point is a corollary of the second.
+\end{proof}
+\noindent
+For convenience again,
+we define $\bmkepss$ on a list $rs$,
+which extracts the bit-codes on the first $\bnullable$ element in $rs$:
+\begin{center}
+	\begin{tabular}{lcl}
+		$\bmkepss \; [] $ & $\dn$ & $[]$\\
+		$\bmkepss \; r :: rs$ & $\dn$ & $\textit{if} \;(\bnullable \; r) \;\; 
+		\textit{then} \;\; \bmkeps \; r \; \textit{else} \;\; \bmkepss \; rs$
+	\end{tabular}
+\end{center}
+\noindent
+If both regular expressions in a rewriting relation are nullable, then they 
+produce the same bitcodes:
+\begin{lemma}\label{rewriteBmkepsAux}
+	\hspace{0em}
+	\begin{itemize}
+		\item
+			$r_1 \rightsquigarrow r_2 \implies 
+			(\bnullable \; r_1 \land \bnullable \; r_2 \implies \bmkeps \; r_1 = 
+			\bmkeps \; r_2)$ 
+		\item
+			and
+			$rs_ 1 \stackrel{s}{\rightsquigarrow} rs_2 
+			\implies (\bnullables \; rs_1 \land \bnullables \; rs_2 \implies 
+			\bmkepss \; rs_1 = \bmkepss \; rs2)$
+	\end{itemize}
+\end{lemma}
+\begin{proof}
+	By rule induction over the cases that lead to $r_1 \rightsquigarrow r_2$.
+\end{proof}
+\noindent
+With lemma \ref{rewriteBmkepsAux} we are ready to prove its
+many-step version: 
+\begin{lemma}
+	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r' \;\; \text{and} \;\; \bnullable \; r, \;\;\; \text{then} \;\; \bmkeps \; r = \bmkeps \; r'$
+\end{lemma}
+\begin{proof}
+	By rule induction of $\stackrel{*}{\rightsquigarrow} $.
+	$\ref{rewritesBnullable}$ tells us both $r$ and $r'$ are nullable.
+	\ref{rewriteBmkepsAux} solves the inductive case.
+\end{proof}
 
-
-Now we get to the "meaty" part of the proof, which relates the relations $\stackrel{s*}{\rightsquigarrow}$ and 
-$\stackrel{*}{\rightsquigarrow} $ with our simplification components such $\distinctBy$ and $\flts$.
-The first lemma below says that for a list made of two parts $rs_1 @ rs_2$, one can throw away the duplicate
-elements in $rs_2$, as well as those that have appeared in $rs_1$:
+\subsubsection{Property 2: $r \stackrel{*}{\rightsquigarrow} \bsimp{r}$}
+Now we get to the ``meaty'' part of the proof, 
+which says that our simplification's helper functions 
+such as $\distinctBy$ and $\flts$ conform to 
+the $\stackrel{s*}{\rightsquigarrow}$ and 
+$\rightsquigarrow^* $ rewriting relations.\\
+The first lemma to prove is a more general version of 
+$rs_ 1 \rightsquigarrow^* \distinctBy \; rs_1 \; \phi$:
 \begin{lemma}
-	$rs_1 @ rs_2 \stackrel{s*}{\rightsquigarrow} (rs_1 @ (\distinctBy \; rs_2 \; \; \rerase{\_}\;  \; (\map\;\; \rerase{\_}\; \; rs_1)))$
+	$rs_1 @ rs_2 \stackrel{s*}{\rightsquigarrow} 
+	(rs_1 @ (\distinctBy \; rs_2 \; \; \rerases \;\; (\map\;\; \rerases \; \; rs_1)))$
 \end{lemma}
+\noindent
+It says that that for a list made of two parts $rs_1 @ rs_2$, 
+one can throw away the duplicate
+elements in $rs_2$, as well as those that have appeared in $rs_1$.
 \begin{proof}
 	By induction on $rs_2$, where $rs_1$ is allowed to be arbitrary.
 \end{proof}
-The above h as the corollary that is suitable for the actual way $\distinctBy$ is called in $\bsimp$:
-\begin{lemma}\label{dBPreserves}
-	$rs_ 1 \rightarrow \distinctBy \; rs_1 \; \phi$
-\end{lemma}
+\noindent
+Setting $rs_2$ to be empty,
+we get the corollary
+\begin{corollary}\label{dBPreserves}
+	$rs_1 \stackrel{s*}{\rightsquigarrow} \distinctBy \; rs_1 \; \phi$.
+\end{corollary}
+\noindent
+The flatten function $\flts$ conforms to
+$\stackrel{s*}{\rightsquigarrow}$ as well:
 
-
-
-The flatten function $\flts$ works within the $\rightsquigarrow$ relation:
 \begin{lemma}\label{fltsPreserves}
 	$rs \stackrel{s*}{\rightsquigarrow} \flts \; rs$
 \end{lemma}
-
-The rewriting in many steps property is composible in terms of regular expression constructors:
-\begin{lemma}
-	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies _{bs} r_1 \cdot r_3 \stackrel{*}{\rightsquigarrow} \;  _{bs} r_2 \cdot r_3 \quad $ and 
-$r_3 \stackrel{*}{\rightsquigarrow} r_4 \implies _{bs} r_1 \cdot r_3 \stackrel{*}{\rightsquigarrow} _{bs} \; r_1 \cdot r_4$
-\end{lemma}
-
-The rewriting in many steps properties $\stackrel{*}{\rightsquigarrow}$ and $\stackrel{s*}{\rightsquigarrow}$ is preserved under the function $\fuse$:
-\begin{lemma}
-	$r_1 \stackrel{*}{\rightsquigarrow} r_2 \implies \fuse \; bs \; r_1 \stackrel{*}{\rightsquigarrow} \; \fuse \; bs \; r_2 \quad $ and 
-	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \map \; (\fuse \; bs) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs) \; rs_2$
-\end{lemma}
 \begin{proof}
-	By the properties $r_1 \rightsquigarrow r_2 \implies \fuse \; bs \; r_1 \implies \fuse \; bs \; r_2$ and
-	$rs_2 \stackrel{s}{\rightsquigarrow} rs_3 \implies \map \; (\fuse \; bs) rs_2 \stackrel{s*}{\rightsquigarrow} \map \; (\fuse \; bs)\; rs_3$.
+	By an induction on $rs$.
 \end{proof}
 \noindent
-If we could rewrite a regular expression in many steps to $\ZERO$, then 
-we could also rewrite any sequence containing it to $\ZERO$:
-\begin{lemma}
-	$r_1 \stackrel{*}{\rightsquigarrow} \ZERO \implies _{bs}r_1\cdot r_2 \stackrel{*}{\rightsquigarrow} \ZERO$
-\end{lemma}
-\begin{lemma}
-	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$
-\end{lemma}
-\noindent
 The function $\bsimpalts$ preserves rewritability:
 \begin{lemma}\label{bsimpaltsPreserves}
 	$_{bs} \sum rs \stackrel{*}{\rightsquigarrow} \bsimpalts \; _{bs} \; rs$
 \end{lemma}
 \noindent
-Before we give out the next lemmas, we define a predicate for a list of regular expressions
-having at least one nullable regular expressions:
-\begin{definition}
-	$\textit{bnullables} \; rs \dn  \exists r \in rs. \bnullable r$
-\end{definition}
-The rewriting relation $\rightsquigarrow$ preserves nullability:
-\begin{lemma}
-	$r_1 \rightsquigarrow r_2 \implies  \bnullable \; r_1 = \bnullable \; r_2$ and
-	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \textit{bnullables} \; rs_1 = \textit{bnullables} \; rs_2$
-\end{lemma}
-\begin{proof}
-	By rule induction of $\rightarrow$ and $\stackrel{s}{\rightsquigarrow}$.
-\end{proof}
-So does the many steps rewriting:
-\begin{lemma}\label{rewritesBnullable}
-	$r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies \bnullable \; r_1 = \bnullable \; r_2$
-\end{lemma}
-\begin{proof}
-	By rule induction of $\stackrel{*}{\rightsquigarrow} $.
-\end{proof}
-\noindent
-And if both regular expressions in a rewriting relation are nullable, then they 
-produce the same bit-codes:
-
-\begin{lemma}\label{rewriteBmkepsAux}
-	$r_1 \rightsquigarrow r_2 \implies (\bnullable \; r_1 \land \bnullable \; r_2 \implies \bmkeps \; r_1 = 
-	\bmkeps \; r_2)$ and
-	$rs_ 1 \stackrel{s}{\rightsquigarrow} rs_2 \implies (\bnullables \; rs_1 \land \bnullables \; rs_2 \implies 
-	\bmkepss \; rs_1 = \bmkepss \; rs2)$
-\end{lemma}
-\noindent
-The definition of $\bmkepss$ on list $rs$ is just to extract the bit-codes on the first element in $rs$ that 
-is $bnullable$:
-\begin{center}
-	\begin{tabular}{lcl}
-		$\bmkepss \; [] $ & $\dn$ & $[]$\\
-		$\bmkepss \; r :: rs$ & $\dn$ & $\textit{if} \; \bnullable \; r then \; (\bmkeps \; r) \; \textit{else} \; \bmkepss \; rs$
-	\end{tabular}
-\end{center}
-\noindent
-And now we are ready to prove the key property that if you 
-have two regular expressions, one rewritable in many steps to the other,
-and one of them is $\bnullable$, then they will both yield the same bits under $\bmkeps$:
-\begin{lemma}
-	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r' \;\; \text{and} \;\; \bnullable \; r_1 \;\; \text{then} \;\; \bmkeps \; r = \bmkeps \; r'$
-\end{lemma}
-\begin{proof}
-	By rule induction of $\stackrel{*}{\rightsquigarrow} $, using \ref{rewriteBmkepsAux} and $\ref{rewritesBnullable}$.
-\end{proof}
-\noindent
-\subsubsection{Property 2: $r \stackrel{*}{\rightsquigarrow} \bsimp{r}$}
-the other property is also ready:
+The simplification function
+$\textit{bsimp}$ only transforms the regex $r$ using steps specified by 
+$\rightsquigarrow^*$ and nothing else.
 \begin{lemma}
 	$r \stackrel{*}{\rightsquigarrow} \bsimp{r}$
 \end{lemma}
 \begin{proof}
 	By an induction on $r$.
-The most difficult case would be the alternative case, where we using properties such as \ref{bsimpaltsPreserves} and \ref{fltsPreserves} and \ref{dBPreserves}, we could continuously rewrite a list like:\\
-	$rs \stackrel{s*}{\rightsquigarrow} \map \; \textit{bsimp} \; rs$\\
-	$\ldots \stackrel{s*}{\rightsquigarrow} \flts \; (\map \; \textit{bsimp} \; rs)$\\
-	$\ldots \;\stackrel{s*}{\rightsquigarrow} \distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerase \; \phi$\\
-	Then we could do the following regular expresssion many steps rewrite:\\
-	$ _{bs} \sum \distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerase \; \phi \stackrel{*}{\rightsquigarrow} \bsimpalts \; bs \; (\distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerase \; \phi)$
-	\\
-	
+	The most involved case would be the alternative, 
+	where we use lemmas \ref{bsimpaltsPreserves},
+	\ref{fltsPreserves} and \ref{dBPreserves} to do a series of rewriting:\\
+	\begin{center}
+		\begin{tabular}{lcl}
+			$rs$ &  $\stackrel{s*}{\rightsquigarrow}$ & $ \map \; \textit{bsimp} \; rs$\\
+			     &  $\stackrel{s*}{\rightsquigarrow}$ & $ \flts \; (\map \; \textit{bsimp} \; rs)$\\
+			     &  $\stackrel{s*}{\rightsquigarrow}$ & $ \distinctBy \; 
+			(\flts \; (\map \; \textit{bsimp}\; rs)) \; \rerases \; \phi$\\
+		\end{tabular}
+	\end{center}
+	Using this we derive the following rewrite relation:\\
+	\begin{center}
+		\begin{tabular}{lcl}
+			$r$ & $=$ & $_{bs}\sum rs$\\[1.5ex]
+			    & $\rightsquigarrow^*$ & $\bsimpalts \; bs \; rs$ \\[1.5ex]
+			    & $\rightsquigarrow^*$ & $\ldots$ \\ [1.5ex]
+			    & $\rightsquigarrow^*$ & $\bsimpalts \; bs \; 
+			    (\distinctBy \; (\flts \; (\map \; \textit{bsimp}\; rs)) 
+			    \; \rerases \; \phi)$\\[1.5ex]
+			    %& $\rightsquigarrow^*$ & $ _{bs} \sum (\distinctBy \; 
+				%(\flts \; (\map \; \textit{bsimp}\; rs)) \; \;
+				%\rerases \; \;\phi) $\\[1.5ex]
+			    & $\rightsquigarrow^*$ & $\textit{bsimp} \; r$\\[1.5ex]
+		\end{tabular}
+	\end{center}	
 \end{proof}
 \subsubsection{Property 3: $r_1 \stackrel{*}{\rightsquigarrow}  r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow} r_2 \backslash c$}
-The first thing we prove is that if we could rewrite in one step, then after derivative
-we could rewrite in many steps:
+The rewritability relation 
+$\rightsquigarrow$ is preserved under derivatives--
+it is just that we might need multiple steps 
+where originally only one step was needed.
 \begin{lemma}\label{rewriteBder}
-	$r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$ and
-	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies \map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$
+	$r_1 \rightsquigarrow r_2 \implies r_1 \backslash c \stackrel{*}{\rightsquigarrow}  r_2 \backslash c$ 
+	and
+	$rs_1 \stackrel{s}{\rightsquigarrow} rs_2 \implies 
+	\map \; (\_\backslash c) \; rs_1 \stackrel{s*}{\rightsquigarrow} \map \; (\_ \backslash c) \; rs_2$
 \end{lemma}
 \begin{proof}
 	By induction on $\rightsquigarrow$ and $\stackrel{s}{\rightsquigarrow}$, using a number of the previous lemmas.
@@ -868,7 +918,9 @@
 	If two regular expressions are rewritable, then they produce the same bits.
 	Under the condition that $ r_1$ is nullable, we have
 	$\text{If} \;\; r \stackrel{*}{\rightsquigarrow} r', \;\;\text{then} \;\; \bmkeps \; r = \bmkeps \; r'$.
-	This proves the \emph{if} (interesting) branch of
+	We have that 
+	$\bmkeps \; (r \backslash s) = \bmkeps \; \bderssimp{r}{s}$ holds.
+	This proves the \emph{if}  branch of
 	$\blexer \; r \; s = \blexersimp{r}{s}$.
 
 \end{proof}