# HG changeset patch
# User Chengsong
# Date 1578781047 0
# Node ID 4a327e70d5382bf136fc8065ee95f4a7dcf38404
# Parent  397b31867ea63f6a054c8863104f12539ee33420
b

diff -r 397b31867ea6 -r 4a327e70d538 Spiral.scala
--- a/Spiral.scala	Fri Jan 10 22:35:08 2020 +0000
+++ b/Spiral.scala	Sat Jan 11 22:17:27 2020 +0000
@@ -571,7 +571,7 @@
       bsimp_print(easy)
     }
     println(bits_print(bsimp(bders(s.toList, internalise(r)))))
-    println(bits_print(ders_simp(internalise(r), s.toList))
+    println(bits_print(ders_simp(internalise(r), s.toList)))
   }
   def find_re(){
     for (i <- 1 to 10000){
diff -r 397b31867ea6 -r 4a327e70d538 etnms/etnms.tex
--- a/etnms/etnms.tex	Fri Jan 10 22:35:08 2020 +0000
+++ b/etnms/etnms.tex	Sat Jan 11 22:17:27 2020 +0000
@@ -33,6 +33,7 @@
 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
 \newcommand{\ZERO}{\mbox{\bf 0}}
 \newcommand{\ONE}{\mbox{\bf 1}}
+\def\erase{\textit{erase}}
 \def\bders{\textit{bders}}
 \def\lexer{\mathit{lexer}}
 \def\blexer{\textit{blexer}}
@@ -297,15 +298,15 @@
 $\retrieve \; a \; v$ is not always defined.
 for example,
 $\retrieve \; _0(_1a+_0a) \; \Left(\Empty)$
-is defined, but not $\retrieve \; _{01}a \;\Left(\Empty)$,
+is defined, but not $\retrieve \; (_{01}a) \;\Left(\Empty)$,
 though we can extract the same POSIX
 bits from the two annotated regular expressions.
 The latter might occur when we try to retrieve from 
 a simplified regular expression using the same value
 as the unsimplified one.
 This is because $\Left(\Empty)$ corresponds to
-the regular expression structure $\AALTS$ instead of
-$\AONE$, this v
+the regular expression structure $\ONE+r_2$ instead of
+$\ONE$.
 That means, if we 
 want to prove that 
 \begin{center}
@@ -316,16 +317,77 @@
 we probably need to prove an equality like below:
 \begin{center}
 %$\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash_{simp} s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
-$\retrieve \; \rup\backslash_{simp} s \; \mkeps(r\backslash s)=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
+$\retrieve \; \rup\backslash_{simp} s \; \mkeps(f(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
 \end{center}
 \noindent
-we would need to rectify the value $\mkeps(r\backslash s)$ into something simpler
+$f$ rectifies $r\backslash s$ so the value $\mkeps(f(r\backslash s))$ becomes
+ something simpler
 to make the retrieve function defined.\\
 One way to do this is to prove the following:
 \begin{center}
 $\retrieve \; \rup\backslash_{simp} s \; \mkeps(\simp(r\backslash s))=\textit{retrieve} \; \rup\backslash s \; \mkeps(r\backslash s)$
 \end{center}
 \noindent
+The reason why we choose $\simp$ as $f$ is because
+$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash \, s)$
+have the same shape:
+\begin{center}
+$\erase (\rup\backslash_{simp} \, s) = \erase(\simp(\rup\backslash s))$
+\end{center}
+
+\noindent
+$\erase$ in the above equality means to remove the bit-codes
+in an annotated regular expression and only keep the original
+regular expression(just like "erasing" the bits). Its definition is omitted.
+$\rup\backslash_{simp} \, s$ and $\simp(\rup\backslash s)$
+are very closely related, but not identical.
+For example, let $r$ be the regular expression
+$(a+b)(a+a*)$ and $s$  be the string $aa$, then
+\begin{center}
+$\rup\backslash_{simp} \, s$ is equal to $_0(_0\ONE +_{11}a^*)$
+\end{center}
+\noindent
+whereas
+\begin{center}
+$\rup\backslash \, s$ is equal to $(_{00}\ONE +_{011}a^*)$
+\end{center}
+\noindent
+Two "rules" might be inferred from the above example.
+First, after erasing the bits the two regular expressions
+are exactly the same: both become $1+a^*$. Here the 
+function $\simp$ exhibits the "once equals many times"
+property: one simplification in the end causes the 
+same regular expression structure as
+ successive simplifications done alongside derivatives.
+Second, the bit-codes are different, but they are essentially
+the same: if we push the outmost bits ${\bf_0}(_0\ONE +_{11}a^*)$ of $\rup\backslash_{simp} \, s$
+inside then we get $(_{00}\ONE +_{011}a^*)$, exactly the 
+same as that of $\rup\backslash \, s$. And this difference 
+does not matter when we try to apply $\bmkeps$ or $\retrieve$
+to it.\\
+If we look into the difference above, we could see why:
+
+that is to say, despite the bits are being moved around on the regular expression
+(difference in bits), the structure of the (unannotated)regular expression
+after one simplification is exactly the same after the 
+same sequence of derivative operations 
+regardless of whether we did simplification
+along the way.
+However, without erase the above equality does not hold:
+for the regular expression  
+$(a+b)(a+a*)$,
+if we do derivative with respect to string $aa$,
+we get
+%TODO
+sdddddr does not equal sdsdsdsr sometimes.\\
+For example,
+
+This equicalence class method might still have the potential of proving this,
+but not yet
+i parallelly tried another method of using retrieve\\
+
+
+
 %HERE CONSTRUCTION SITE
 The vsimp function, defined as follows
 tries to simplify the value in lockstep with