--- a/etnms/etnms.tex Fri Jan 17 23:53:08 2020 +0000
+++ b/etnms/etnms.tex Mon Jan 20 15:51:06 2020 +0000
@@ -494,6 +494,8 @@
basic regular expressions, except that we beed to take care of
the bitcodes:
+
+\iffalse
%\begin{definition}{bder}
\begin{center}
\begin{tabular}{@{}lcl@{}}
@@ -516,6 +518,49 @@
\end{center}
%\end{definition}
+\begin{center}
+ \begin{tabular}{@{}lcl@{}}
+ $(\textit{ZERO})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
+ $(_{bs}\textit{ONE})\,\backslash c$ & $\dn$ & $\textit{ZERO}$\\
+ $(_{bs}\textit{CHAR}\;d)\,\backslash c$ & $\dn$ &
+ $\textit{if}\;c=d\; \;\textit{then}\;
+ _{bs}\textit{ONE}\;\textit{else}\;\textit{ZERO}$\\
+ $(_{bs}\textit{ALTS}\;as)\,\backslash c$ & $\dn$ &
+ $_{bs}\textit{ALTS}\;(as.map(\backslash c))$\\
+ $(_{bs}\textit{SEQ}\;a_1\,a_2)\,\backslash c$ & $\dn$ &
+ $\textit{if}\;\textit{bnullable}\,a_1$\\
+ & &$\textit{then}\;_{bs}\textit{ALTS}\,List((_{[]}\textit{SEQ}\,(a_1\,\backslash c)\,a_2),$\\
+ & &$\phantom{\textit{then}\;_{bs}\textit{ALTS}\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
+ & &$\textit{else}\;_{bs}\textit{SEQ}\,(a_1\,\backslash c)\,a_2$\\
+ $(_{bs}\textit{STAR}\,a)\,\backslash c$ & $\dn$ &
+ $_{bs}\textit{SEQ}\;(\textit{fuse}\, [\Z] (r\,\backslash c))\,
+ (_{bs}\textit{STAR}\,[]\,r)$
+\end{tabular}
+\end{center}
+%\end{definition}
+\fi
+
+\begin{center}
+ \begin{tabular}{@{}lcl@{}}
+ $(\ZERO)\,\backslash c$ & $\dn$ & $\ZERO$\\
+ $(_{bs}\ONE)\,\backslash c$ & $\dn$ & $\ZERO$\\
+ $(_{bs}{\bf d})\,\backslash c$ & $\dn$ &
+ $\textit{if}\;c=d\; \;\textit{then}\;
+ _{bs}\ONE\;\textit{else}\;\ZERO$\\
+ $(_{bs}\oplus \;as)\,\backslash c$ & $\dn$ &
+ $_{bs}\oplus\;(as.map(\backslash c))$\\
+ $(_{bs}\;a_1\cdot a_2)\,\backslash c$ & $\dn$ &
+ $\textit{if}\;\textit{bnullable}\,a_1$\\
+ & &$\textit{then}\;_{bs}\oplus\,[(_{[]}\,(a_1\,\backslash c)\cdot\,a_2),$\\
+ & &$\phantom{\textit{then},\;_{bs}\oplus\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))]$\\
+ & &$\textit{else}\;_{bs}\,(a_1\,\backslash c)\cdot a_2$\\
+ $(_{bs}a^*)\,\backslash c$ & $\dn$ &
+ $_{bs}\;((\textit{fuse}\, [\Z] (r\,\backslash c))\cdot
+ (_{[]}r^*))$
+\end{tabular}
+\end{center}
+
+%\end{definition}
\noindent
For instance, when we unfold $\textit{STAR} \; bs \; a$ into a sequence,
we need to attach an additional bit $Z$ to the front of $r \backslash c$
@@ -1197,6 +1242,7 @@
if we do derivative with respect to string $aa$,
we get
+\subsection{Another Proof Strategy}
sdddddr does not equal sdsdsdsr sometimes.\\
For example,