diff -r ba40ab3658ca -r 51ac1ab6e1fd ninems/ninems.tex
--- a/ninems/ninems.tex	Thu Jul 25 12:59:07 2019 +0100
+++ b/ninems/ninems.tex	Thu Jul 25 21:02:06 2019 +0100
@@ -872,14 +872,14 @@
 Sulzmann and Lu's integrated the bitcodes into regular expressions to
 create annotated regular expressions \cite{Sulzmann2014}.
 \emph{Annotated regular expressions} are defined by the following
-grammar:\comment{ALTS should have  an $as$ in  the definitions, not  just $a_1$ and $a_2$}
+grammar:%\comment{ALTS should have  an $as$ in  the definitions, not  just $a_1$ and $a_2$}
 
 \begin{center}
 \begin{tabular}{lcl}
   $\textit{a}$ & $::=$  & $\textit{ZERO}$\\
                   & $\mid$ & $\textit{ONE}\;\;bs$\\
                   & $\mid$ & $\textit{CHAR}\;\;bs\,c$\\
-                  & $\mid$ & $\textit{ALTS}\;\;bs\,a_1 \, a_2$\\
+                  & $\mid$ & $\textit{ALTS}\;\;bs\,as$\\
                   & $\mid$ & $\textit{SEQ}\;\;bs\,a_1\,a_2$\\
                   & $\mid$ & $\textit{STAR}\;\;bs\,a$
 \end{tabular}    
@@ -887,8 +887,11 @@
 %(in \textit{ALTS})
 
 \noindent
-where $bs$ stands for bitcodes, and $a$  for $\bold{a}$nnotated regular
-expressions. We will show that these bitcodes encode information about
+where $bs$ stands for bitcodes, $a$  for $\bold{a}$nnotated regular
+expressions and $as$ for a list of annotated regular expressions.
+The alternative constructor($\textit{ALTS}$) has been generalized to 
+accept a list of annotated regular expressions rather than just 2.
+We will show that these bitcodes encode information about
 the (POSIX) value that should be generated by the Sulzmann and Lu
 algorithm.
 
@@ -905,8 +908,8 @@
   $(\ONE)^\uparrow$ & $\dn$ & $\textit{ONE}\,[]$\\
   $(c)^\uparrow$ & $\dn$ & $\textit{CHAR}\,[]\,c$\\
   $(r_1 + r_2)^\uparrow$ & $\dn$ &
-         $\textit{ALTS}\;[]\,(\textit{fuse}\,[\Z]\,r_1^\uparrow)\,
-                            (\textit{fuse}\,[\S]\,r_2^\uparrow)$\\
+  $\textit{ALTS}\;[]\,List((\textit{fuse}\,[\Z]\,r_1^\uparrow),\,
+  (\textit{fuse}\,[\S]\,r_2^\uparrow))$\\
   $(r_1\cdot r_2)^\uparrow$ & $\dn$ &
          $\textit{SEQ}\;[]\,r_1^\uparrow\,r_2^\uparrow$\\
   $(r^*)^\uparrow$ & $\dn$ &
@@ -929,8 +932,8 @@
      $\textit{ONE}\,(bs\,@\,bs')$\\
   $\textit{fuse}\;bs\,(\textit{CHAR}\,bs'\,c)$ & $\dn$ &
      $\textit{CHAR}\,(bs\,@\,bs')\,c$\\
-  $\textit{fuse}\;bs\,(\textit{ALTS}\,bs'\,a_1\,a_2)$ & $\dn$ &
-     $\textit{ALTS}\,(bs\,@\,bs')\,a_1\,a_2$\\
+  $\textit{fuse}\;bs\,(\textit{ALTS}\,bs'\,as)$ & $\dn$ &
+     $\textit{ALTS}\,(bs\,@\,bs')\,as$\\
   $\textit{fuse}\;bs\,(\textit{SEQ}\,bs'\,a_1\,a_2)$ & $\dn$ &
      $\textit{SEQ}\,(bs\,@\,bs')\,a_1\,a_2$\\
   $\textit{fuse}\;bs\,(\textit{STAR}\,bs'\,a)$ & $\dn$ &
@@ -953,12 +956,12 @@
   $(\textit{CHAR}\;bs\,d)\,\backslash c$ & $\dn$ &
         $\textit{if}\;c=d\; \;\textit{then}\;
          \textit{ONE}\;bs\;\textit{else}\;\textit{ZERO}$\\  
-  $(\textit{ALTS}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
-        $\textit{ALTS}\;bs\,(a_1\,\backslash c)\,(a_2\,\backslash c)$\\
+  $(\textit{ALTS}\;bs\,as)\,\backslash c$ & $\dn$ &
+  $\textit{ALTS}\;bs\,(as.map(\backslash c))$\\
   $(\textit{SEQ}\;bs\,a_1\,a_2)\,\backslash c$ & $\dn$ &
      $\textit{if}\;\textit{bnullable}\,a_1$\\
-  & &$\textit{then}\;\textit{ALTS}\,bs\,(\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2)$\\
-  & &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c))$\\
+					       & &$\textit{then}\;\textit{ALTS}\,bs\,List((\textit{SEQ}\,[]\,(a_1\,\backslash c)\,a_2),$\\
+					       & &$\phantom{\textit{then}\;\textit{ALTS}\,bs\,}(\textit{fuse}\,(\textit{bmkeps}\,a_1)\,(a_2\,\backslash c)))$\\
   & &$\textit{else}\;\textit{SEQ}\,bs\,(a_1\,\backslash c)\,a_2$\\
   $(\textit{STAR}\,bs\,a)\,\backslash c$ & $\dn$ &
       $\textit{SEQ}\;bs\,(\textit{fuse}\, [\Z] (r\,\backslash c))\,
@@ -993,10 +996,10 @@
 \begin{center}
 \begin{tabular}{lcl}
   $\textit{bmkeps}\,(\textit{ONE}\;bs)$ & $\dn$ & $bs$\\
-  $\textit{bmkeps}\,(\textit{ALTS}\;bs\,a_1\,a_2)$ & $\dn$ &
-     $\textit{if}\;\textit{bnullable}\,a_1$\\
-  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a_1$\\
-  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,a_2$\\
+  $\textit{bmkeps}\,(\textit{ALTS}\;bs\,a::as)$ & $\dn$ &
+     $\textit{if}\;\textit{bnullable}\,a$\\
+  & &$\textit{then}\;bs\,@\,\textit{bmkeps}\,a$\\
+  & &$\textit{else}\;bs\,@\,\textit{bmkeps}\,(\textit{ALTS}\;bs\,as)$\\
   $\textit{bmkeps}\,(\textit{SEQ}\;bs\,a_1\,a_2)$ & $\dn$ &
      $bs \,@\,\textit{bmkeps}\,a_1\,@\, \textit{bmkeps}\,a_2$\\
   $\textit{bmkeps}\,(\textit{STAR}\;bs\,a)$ & $\dn$ &
@@ -1100,7 +1103,7 @@
 these two operations as an atomic one: $a \backslash_{simp}\,c \dn
 \textit{simp}(a \backslash c)$. Then we can use the previous natural
 extension from derivative w.r.t.~character to derivative
-w.r.t.~string:\comment{simp in  the [] case?}
+w.r.t.~string:%\comment{simp in  the [] case?}
 
 \begin{center}
 \begin{tabular}{lcl}
@@ -1157,8 +1160,9 @@
 We like to settle this correctness claim. It is relatively
 straightforward to establish that after one simplification step, the part of a
 nullable derivative that corresponds to a POSIX value remains intact and can
-still be collected, in other words, we can show that\comment{Double-check....I
-think this  is not the case}
+still be collected, in other words, we can show that
+%\comment{Double-check....I
+%think this  is not the case}
 %\comment{If i remember correctly, you have proved this lemma.
 %I feel this is indeed not true because you might place arbitrary 
 %bits on the regex r, however if this is the case, did i remember wrongly that
@@ -1177,7 +1181,8 @@
 
 \begin{center}
 	$ \textit{blexer}\_{simp}(r, \; s) =  \textit{blexer}(r, \; s)$
-\end{center}\comment{This is not true either...look at the definion blexer/blexer-simp}
+\end{center}
+%comment{This is not true either...look at the definion blexer/blexer-simp}
 
 \noindent That is, if we do derivative on regular expression $r$ and then
 simplify it, and repeat this process until we exhaust the string, we get a
@@ -1197,8 +1202,26 @@
 augmented and propagated 
 during simplification in parallel with the regular expression that
 has not been simplified in the subsequent derivative operations.  To aid this,
-we use the helper function retrieve described by Sulzmann and Lu: \\definition
-of retrieve TODO\comment{Did not read further}\\
+we use the helper function retrieve described by Sulzmann and Lu:
+\begin{center}
+\begin{tabular}{@{}l@{\hspace{2mm}}c@{\hspace{2mm}}l@{}}
+  $\textit{retrieve}\,(\textit{ONE}\,bs)\,\Empty$ & $\dn$ & $bs$\\
+  $\textit{retrieve}\,(\textit{CHAR}\,bs\,c)\,(\Char\,d)$ & $\dn$ & $bs$\\
+  $\textit{retrieve}\,(\textit{ALTS}\,bs\,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$ &
+     $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$ &\\
+  \multicolumn{3}{l}{
+     \hspace{3cm}$bs \,@\, [\Z] \,@\, \textit{retrieve}\,a\,v\,@\,
+                    \textit{retrieve}\,(\textit{STAR}\,[]\,a)\,(\Stars\,vs)$}\\
+\end{tabular}
+\end{center}
+%\comment{Did not read further}\\
 This function assembles the bitcode 
 %that corresponds to a lexical value for how
 %the current derivative matches the suffix of the string(the characters that