# HG changeset patch
# User Chengsong
# Date 1583172492 0
# Node ID 31711ca3168513be5dc8ca8b4ced9850030dc5f0
# Parent  13a42b418eabfd8fc17afdeafeea4ce590403938
contains section finished

diff -r 13a42b418eab -r 31711ca31685 etnms/etnms.tex
--- a/etnms/etnms.tex	Sun Mar 01 20:12:16 2020 +0000
+++ b/etnms/etnms.tex	Mon Mar 02 18:08:12 2020 +0000
@@ -1654,13 +1654,47 @@
 \end{center}
 Here $\gg$ is almost like an $\textit{NFA}$ in the sense that 
 it simulates the lexing process with respect to different strings.
-\end{itemize}
+
 Our hope is that using $\gg$ we can prove the bits
 information are not lost when we simplify a regular expression,
 so we need to relate $\gg$ with simplifcation, for example, 
 one of the lemmas we have proved about $\gg$ is that
- 
-$\simp$
+\item
+\begin{center}
+$\simp \; a \gg \textit{bs} \iff  a \gg \textit{bs}$
+\end{center}
+This could be a step towards our goal, as
+it assures that after simplification none of the 
+bitsequence that can be created by
+the original annotated regular expression
+is lost.
+If we could prove the following that would be
+another step towards our proof, 
+
+\item
+\begin{center}
+$(\simp \;a) \backslash s \gg \textit{bs} \iff  a\backslash s \gg \textit{bs}$
+\end{center}
+
+as it says
+the simplified regular expression after derivatives will 
+still have the full capacity of producing bitsequences
+as the unsimplified ones-- pretty much
+the intuition we try to establish.
+And if we could prove
+\item
+\begin{center}
+$a \backslash s \gg \textit{bs} \iff  a\backslash_\textit{simp} s \gg \textit{bs}$
+\end{center}
+That would be just a stone's throw away
+from $\blexer \; r \; s = \blexers \; r \; s$.
+
+\end{itemize}
+What we do after we work out 
+the proof of the above lemma 
+is still not clear. It is one of the next steps we need to 
+work on.
+
 \subsection{the $\textit{ders}_2$ Function}
 If we want to prove the result 
 \begin{center}
@@ -1670,8 +1704,9 @@
 on the structure of the regular expression,
 then we need to induct on the  case $r_1 \cdot r_2$,
 it can be good if we could express $(r_1 \cdot r_2) \backslash s$
-in terms of $r_1 \backslash s$ and $r_2 \backslash s$,
-and this naturally induces the $ders2$ function,
+in terms of $r_1 \backslash s_1$ and $r_2 \backslash s_1$,
+where $s_1$ is a substring of $s$.
+For this we introduce the $\textit{ders2}$ function,
 which does a "convolution" on $r_1$ and $r_2$ using the string
 $s$.
 It is based on the observation that the derivative of $r_1 \cdot r_2$