--- a/Spiral.scala	Fri Jan 17 23:53:08 2020 +0000
+++ b/Spiral.scala	Mon Jan 20 15:51:06 2020 +0000
@@ -840,13 +840,25 @@
       }
     }
   }
-
+  def have_fun(){
+    val bis = List(S,S)
+    val bits = List(S,S,Z)
+    val reg = ("a" | (("a")%) )~("b")
+    val res = decode_aux(reg, bis)
+    val result = decode_aux(reg, bis)
+    val result1 = decode_aux(reg, List(Z))
+    println(res)
+    println(result)
+    println(bsimp(bders( "a".toList, internalise(reg))))
+    println(result1)
+  }
   def main(args: Array[String]) {
     //println(S.toString)
     //find_re()
     //tellmewhy()
     //correctness_proof_convenient_path()
-    tellmewhy()
+    //tellmewhy()
+    have_fun()
     //string_der_test()
     //comp(rd_string_gen(3,6).toList, random_struct_gen(7))
     //newxp1()

--- 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,
 

--- a/lex_blex_Frankensteined.scala	Fri Jan 17 23:53:08 2020 +0000
+++ b/lex_blex_Frankensteined.scala	Mon Jan 20 15:51:06 2020 +0000
@@ -119,6 +119,7 @@
       val (v, bs1) = decode_aux(r1, bs)
       (Rec(x, v), bs1)
     }
+    case (r, Nil) => (Stars(Nil), Nil)
   }
 
   def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {