# HG changeset patch
# User Chengsong
# Date 1583093536 0
# Node ID 13a42b418eabfd8fc17afdeafeea4ce590403938
# Parent  eff05af278c0f74926069bc53b605dd471adc8ea
failsafe

diff -r eff05af278c0 -r 13a42b418eab etnms/etnms.tex
--- a/etnms/etnms.tex	Fri Feb 28 22:48:10 2020 +0000
+++ b/etnms/etnms.tex	Sun Mar 01 20:12:16 2020 +0000
@@ -1565,8 +1565,102 @@
 proved about contains:
 \begin{itemize}
 \item
-$\textit{if} \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)$
+\begin{center}
+\begin{equation}\label{contains1}
+\textit{if}\; \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)
+\end{equation}
+\end{center}
+This lemma states that the set
+$\{\textit{bs}\; | \rup \gg \textit{bs} \}$ 
+"contains" all the underlying value $v$ of $r$ in which they are 
+in a coded form.
+These values include the ones created in the 
+lexing process, for example, when the regular
+expression $r$ is nullable, then we have:
+\item
+\begin{center}
+$r \gg \textit{bmkeps}(r)$
+\end{center}
+This can be seen as a corollary of the previous lemma,
+because $\models \textit{mkeps}((r\downarrow)):(r\downarrow)$
+and $\textit{code}(\mkeps((r\downarrow))) = \bmkeps(r)$.
+Another corollary we have of \eqref{contains1}
+\item
+\begin{center}
+$\textit{if}\; \models v:r \; \textit{then} \; \rup \gg \textit{retrieve} \; \rup \; v$
+\end{center}
+as $\textit{retrieve} \; \rup \; v = \textit{code}(v)$
+It says that if you can extract a bitsequence using 
+retrieve guided by $v$, then such bitsequence is already there in the set 
+$\{\textit{bs}\; | \rup \gg \textit{bs} \}$.
+This lemma has a slightly different form:
+\item
+\begin{center}
+$\textit{if}\; \models v:a\downarrow \; \textit{then} \; a \gg \textit{retrieve} \; a \; v$
+\end{center}
+This is almost identical to the previous lemma, except
+this time we might have arbitrary bits attached 
+to anywhere of the annotated regular expression $a$.
+$a$ can be any "made up" annotated regular expressions
+that does not belong to the "natural" ones created by 
+internalising an unannotated regular expression.
+For example, a regular expression $r = (a+b)$ after internalisation
+becomes $\rup = (_0a+_1b)$. For an underlying value $v = \Left(\Char(a))$
+we have $\retrieve \; (_0a+_1b) \;v = 0$ and $(_0a+_1b) \gg 0$. We could 
+attach arbitrary bits to the regular expression $\rup$
+without breaking the structure,
+ for example  we could make up $a = _{0100111}(_{1011}a+1b)$,
+ and we still have $\models v:a\downarrow$, and
+ therefore  $a \gg \retrieve \; a \; v$, this time the bitsequence
+ being $01001111011$.
+This shows that the inductive clauses defining $\gg$
+simulates what $\retrieve$ does guided by different 
+values.
+Set $\{\textit{bs}\; | \rup \gg \textit{bs} \}$ contains
+a wide range of values coded as bitsequences,
+the following property can be routinely established 
+from the previous lemma
+\item
+\begin{center}
+$r \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v) \;\;\; \textit{if} \; \models v: \textit{der} \; c \; (\erase(r))$
+\end{center}
+because $\inj \; (r\downarrow)\; c\; v$ is a value
+underlying $r$.
+Using this we can get something that looks much
+less obvious:
+\item
+
+\begin{center}
+\begin{tabular}{c}
+$\textit{if} \models v: \erase(r)\backslash c \; \textit{then}$\\
+$r\backslash c \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v) \; \textit{and}$\\
+$r \gg \retrieve \; r \; (\inj \; (r\downarrow) \; c \; v)$\\
+\end{tabular}
+\end{center}
+It says that the derivative operation $\backslash c$ is basically
+an operation that does not change the bits an annotated regular
+expression is able to produce, both
+$r\backslash c$ and $r$ can produce 
+the bitsequence $\inj \; (r\downarrow) \; c \;v)$.
+This invariance with respect to derivative can be
+further extended to a more surprising property:
+\item
+\begin{center}
+\begin{tabular}{c}
+$\textit{if} \models v: \erase(r) \backslash s$\\
+$r\backslash s \gg \retrieve \; r \; (\flex \; (r\downarrow) \; \textit{id} \; s \; v) \; \textit{and}$\\
+$r \gg \retrieve \; r \; (r\downarrow) \; \textit{id} \; s \; v) \; c \; v)$\\
+\end{tabular}
+\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$
 \subsection{the $\textit{ders}_2$ Function}
 If we want to prove the result 
 \begin{center}