--- a/etnms/etnms.tex	Wed Feb 05 12:02:21 2020 +0000
+++ b/etnms/etnms.tex	Wed Feb 05 12:41:30 2020 +0000
@@ -598,11 +598,11 @@
   $\textit{bmkeps}\,(_{bs}\oplus a::\textit{as})$ & $\dn$ &
      $\textit{if}\;\textit{bnullable}\,a$\\
   & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
-  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\textit{as})$\\
+  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(_{bs}\oplus \textit{as})$\\
   $\textit{bmkeps}\,(_{bs} a_1 \cdot a_2)$ & $\dn$ &
      $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
   $\textit{bmkeps}\,(_{bs}a^*)$ & $\dn$ &
-     $bs \,@\, [1]$
+     $bs \,@\, [0]$
 \end{tabular}    
 \end{center}    
 %\end{definition}
@@ -642,7 +642,7 @@
 expressions and strings. 
 
 One modification we introduced is to allow a list of annotated regular
-expressions in the \textit{ALTS} constructor. This allows us to not just
+expressions in the $\oplus$ constructor. This allows us to not just
 delete unnecessary $\ZERO$s and $\ONE$s from regular expressions, but
 also unnecessary ``copies'' of regular expressions (very similar to
 simplifying $r + r$ to just $r$, but in a more general setting). Another
@@ -658,17 +658,17 @@
 \begin{center}
   \begin{tabular}{@{}lcl@{}}
    
-  $\textit{simp} \; (\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ & $ (\textit{simp} \; a_1, \textit{simp}  \; a_2) \; \textit{match} $ \\
+  $\textit{simp} \; (_{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{SEQ} \; bs \; a_1' \;  a_2'$ \\
+   &&$\quad\textit{case} \; (a_1', a_2') \Rightarrow   _{bs}a_1' \cdot a_2'$ \\
 
-  $\textit{simp} \; (\textit{ALTS}\;bs\,as)$ & $\dn$ & $\textit{distinct}( \textit{flatten} ( \textit{map simp as})) \; \textit{match} $ \\
+  $\textit{simp} \; (_{bs}\oplus \textit{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'$\\ 
+   &&$\quad\textit{case} \;  as' \Rightarrow _{bs}\oplus \textit{as'}$\\ 
 
    $\textit{simp} \; a$ & $\dn$ & $\textit{a} \qquad \textit{otherwise}$   
 \end{tabular}    
@@ -680,19 +680,19 @@
 sequence, it will try to simplify its children regular expressions
 recursively and then see if one of the children turn into $\ZERO$ or
 $\ONE$, which might trigger further simplification at the current level.
-The most involved part is the $\textit{ALTS}$ clause, where we use two
+The most involved part is the $\oplus$ clause, where we use two
 auxiliary functions $\textit{flatten}$ and $\textit{distinct}$ to open up nested
-$\textit{ALTS}$ and reduce as many duplicates as possible. Function
+alternatives and reduce as many duplicates as possible. Function
 $\textit{distinct}$  keeps the first occurring copy only and remove all later ones
-when detected duplicates. Function $\textit{flatten}$ opens up nested \textit{ALTS}.
+when detected duplicates. Function $\textit{flatten}$ opens up nested $\oplus$s.
 Its recursive definition is given below:
 
  \begin{center}
   \begin{tabular}{@{}lcl@{}}
-  $\textit{flatten} \; (\textit{ALTS}\;bs\,as) :: as'$ & $\dn$ & $(\textit{map} \;
+  $\textit{flatten} \; (_{bs}\oplus \textit{as}) :: \textit{as'}$ & $\dn$ & $(\textit{map} \;
      (\textit{fuse}\;bs)\; \textit{as}) \; @ \; \textit{flatten} \; as' $ \\
-  $\textit{flatten} \; \textit{ZERO} :: as'$ & $\dn$ & $ \textit{flatten} \;  as' $ \\
-    $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; as'$ \quad(otherwise) 
+  $\textit{flatten} \; \ZERO :: as'$ & $\dn$ & $ \textit{flatten} \;  \textit{as'} $ \\
+    $\textit{flatten} \; a :: as'$ & $\dn$ & $a :: \textit{flatten} \; \textit{as'}$ \quad(otherwise) 
 \end{tabular}    
 \end{center}  
 
@@ -936,18 +936,18 @@
 \begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
   $\textit{retrieve}\,(_{bs}\ONE)\,\Empty$ & $\dn$ & $bs$\\
   $\textit{retrieve}\,(_{bs}{\bf c})\,(\Char\,d)$ & $\dn$ & $bs$\\
-  $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Left\,v)$ & $\dn$ &
+  $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Left\,v)$ & $\dn$ &
      $bs \,@\, \textit{retrieve}\,a\,v$\\
-  $\textit{retrieve}\,(\textit{ALTS}\,bs\,a::as)\,(\Right\,v)$ & $\dn$ &
-  $bs \,@\, \textit{retrieve}\,(\textit{ALTS}\,bs\,as)\,v$\\
-  $\textit{retrieve}\,(\textit{SEQ}\,bs\,a_1\,a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
+  $\textit{retrieve}\,(_{bs}\oplus a::as)\,(\Right\,v)$ & $\dn$ &
+  $\textit{bs} \,@\, \textit{retrieve}\,(_{[]}\oplus as)\,v$\\
+  $\textit{retrieve}\,(_{bs}a_1\cdot a_2)\,(\Seq\,v_1\,v_2)$ & $\dn$ &
      $bs \,@\,\textit{retrieve}\,a_1\,v_1\,@\, \textit{retrieve}\,a_2\,v_2$\\
-  $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,[])$ & $\dn$ &
-     $bs \,@\, [\S]$\\
-  $\textit{retrieve}\,(\textit{STAR}\,bs\,a)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
+  $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,[])$ & $\dn$ &
+     $bs \,@\, [0]$\\
+  $\textit{retrieve}\,(_{bs}a^*)\,(\Stars\,(v\!::\!vs))$ & $\dn$ &\\
   \multicolumn{3}{l}{
-     \hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\,
-                    \textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\
+     \hspace{3cm}$bs \,@\, [1] \,@\, \textit{retrieve}\,a\,v\,@\,
+                    \textit{retrieve}\,(_{[]}a^*)\,(\Stars\,vs)$}\\
 \end{tabular}
 \end{center}
 %\comment{Did not read further}\\
@@ -984,15 +984,6 @@
 from $v$ is not so straightforward. The point of this is that  we might
 be able to finally bridge the gap by proving
 
-
-\noindent\rule[1.5ex]{\linewidth}{4pt}
-There is no mention of retrieve yet .... this is the second trick in the
-existing proof. I am not sure whether you need to explain annotated regular
-expressions much earlier - maybe before the ``existing proof'' section, or
-evan earlier.
-
-\noindent\rule[1.5ex]{\linewidth}{4pt}
-
 \noindent
 By using a property of retrieve we have the $\textit{RHS}$ of the above equality is
 $decode (retrieve (r^\uparrow \backslash(s @ [c])) v) r$, and this gives the