diff -r c19f2d20d92c -r 8dbc83ecea3b etnms/etnms.tex
--- a/etnms/etnms.tex	Fri Jan 24 09:27:03 2020 +0000
+++ b/etnms/etnms.tex	Fri Jan 24 18:44:52 2020 +0000
@@ -8,6 +8,7 @@
 \usepackage[noend]{algpseudocode}
 \usepackage{enumitem}
 \usepackage{nccmath}
+\usepackage{soul}
 
 \definecolor{darkblue}{rgb}{0,0,0.6}
 \hypersetup{colorlinks=true,allcolors=darkblue}
@@ -1311,6 +1312,39 @@
 actually prove that simplification function never allows nested
 alternatives to happen, more on this later).
 
+How about we do not allow the function $\simp$
+to fuse out the bits when it is unnecessary?
+Like, for the above regular expression, we might
+just delete the outer layer of alternative
+\begin{center}
+\st{$ {\oplus[\ZERO \;,}$} $_{bs}\oplus \textit{rs}$ \st{$]$}
+\end{center}
+and get $_{bs}\oplus \textit{rs}$ instead, without
+fusing the bits $\textit{bs}$ inside to every element 
+of $\textit{rs}$.
+This idea can be realized by making the following
+changes to the $\simp$-function:
+\begin{center}
+  \begin{tabular}{@{}lcl@{}}
+   
+  $\textit{simp} \; (_{\textit{bs}}(a_1 \cdot a_2))$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\
+   &&$\quad\textit{case} \; (\ZERO, \_) \Rightarrow  \ZERO$ \\
+   &&$\quad\textit{case} \; (\_, \ZERO) \Rightarrow  \ZERO$ \\
+   &&$\quad\textit{case} \;  (\ONE, a_2') \Rightarrow  \textit{fuse} \; bs \;  a_2'$ \\
+   &&$\quad\textit{case} \; (a_1', \ONE) \Rightarrow  \textit{fuse} \; bs \;  a_1'$ \\
+   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow  _{\textit{bs}}(a_1' \cdot a_2')$ \\
+
+  $\textit{simp} \; (bs_\oplus as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
+  &&$\quad\textit{case} \; [] \Rightarrow  \ZERO$ \\
+   &&$\quad\textit{case} \; a :: [] \Rightarrow  \textit{fuse bs a}$ \\
+   &&$\quad\textit{case} \;  as' \Rightarrow  \textit{ALTS}\;bs\;as'$\\ 
+
+   $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
+\end{tabular}    
+\end{center}    
+
+\noindent
+
 \subsection{Properties of the Function $\simp$}
 
 We have proved in Isabelle quite a few properties
@@ -1320,9 +1354,14 @@
 To start, we need a bit of auxiliary notations,
 which is quite basic and is only written here
 for clarity.
-$\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r\}$\\
+
+$\textit{sub}(r)$ computes the set of the 
+sub-regular expression of $r$:
+\begin{center}
+$\textit{sub}(\ONE) \dn \{\ONE\}$\\
+$\textit{sub}(r_1 \cdot r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1 \cdot r_2\}$\\
 $\textit{sub}(r_1 + r_2) \dn \textit{sub}(r_1) \cup \textit{sub}(r_2) \cup \{r_1+r_2\}$\\
-
+\end{center}
 $\textit{good}(r) \dn r \neq \ZERO \land \\
 \forall r' \in \textit{sub}(r), \textit{if} \; r' = _{bs_1}\oplus(rs_1), \;
 \textit{then} \nexists r'' \in \textit{rs}_1 \; s.t.\;