--- 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}