diff -r 0a0c551bb368 -r 79f347cb8b4d etnms/etnms.tex
--- 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,