diff -r 2b95bcd2ac73 -r 9c1ca6d6e190 corr_pr_sketch.tex
--- a/corr_pr_sketch.tex	Sat Mar 23 11:53:09 2019 +0000
+++ b/corr_pr_sketch.tex	Wed Apr 10 16:34:34 2019 +0100
@@ -314,50 +314,129 @@
 
 \begin{theorem}{
 This is a very strong claim that has yet to be more carefully examined and proved. However, experiments suggest a very good hope for this.}\\
-Define pushbits as the following:\\
-$pushbits(r) = if( r == ALTS(bs, rs) )\ then\ ALTS(Nil, rs.map(fuse(bs,\_)))  \ else\ r$.\\
+Define pushbits as the following:\\  
+\begin{verbatim}
+def pushbits(r: ARexp): ARexp = r match {
+    case AALTS(bs, rs) => AALTS(Nil, rs.map(r=>fuse(bs, pushbits(r))))
+    case ASEQ(bs, r1, r2) => ASEQ(bs, pushbits(r1), pushbits(r2))
+    case r => r
+  }
+  \end{verbatim}
 Then we have \mbox{\boldmath$pushbits(ders\_simp(ar, s) ) == simp(ders(ar,s)) \ or\ ders\_simp(ar, s) == simp(ders(ar, s))$}.\\
 Unfortunately this does not hold. A counterexample is\\
 \begin{verbatim}
-r = ASTAR(List(),ASEQ(List(),AALTS(List(),List(ACHAR(List(Z),c), ACHAR(List(S),b))),ASEQ(List(),ASTAR(List(),ACHAR(List(),a)),AALTS(List(),List(ACHAR(List(Z),a), ACHAR(List(S),a))))))
+baa
+original regex
+STA
+ └-ALT
+    └-STA List(Z)
+    |  └-a
+    └-ALT List(S)
+       └-b List(Z)
+       └-a List(S)
 regex after ders simp
-
-SEQ
- └-ALT List(S, S, C(b))
- |  └-SEQ
- |  |  └-STA List(S, C(a), S, C(a))
- |  |  |  └-a
- |  |  └-a List(Z)
- |  └-ONE List(S, C(a), Z, Z, C(a))
- └-STA
+ALT List(S, S, Z, C(b))
+ └-SEQ
+ |  └-STA List(S, Z, S, C(a), S, C(a))
+ |  |  └-a
+ |  └-STA
+ |     └-ALT
+ |        └-STA List(Z)
+ |        |  └-a
+ |        └-ALT List(S)
+ |           └-b List(Z)
+ |           └-a List(S)
+ └-SEQ List(S, Z, S, C(a), Z)
+    └-ALT List(S)
+    |  └-STA List(Z, S, C(a))
+    |  |  └-a
+    |  └-ONE List(S, S, C(a))
+    └-STA
+       └-ALT
+          └-STA List(Z)
+          |  └-a
+          └-ALT List(S)
+             └-b List(Z)
+             └-a List(S)
+regex after ders
+ALT
+ └-SEQ
+ |  └-ALT List(S)
+ |  |  └-SEQ List(Z)
+ |  |  |  └-ZERO
+ |  |  |  └-STA
+ |  |  |     └-a
+ |  |  └-ALT List(S)
+ |  |     └-ZERO
+ |  |     └-ZERO
+ |  └-STA
+ |     └-ALT
+ |        └-STA List(Z)
+ |        |  └-a
+ |        └-ALT List(S)
+ |           └-b List(Z)
+ |           └-a List(S)
+ └-ALT List(S, S, Z, C(b))
     └-SEQ
-       └-ALT
-       |  └-c List(Z)
-       |  └-b List(S)
-       └-SEQ
-          └-STA
-          |  └-a
+    |  └-ALT List(S)
+    |  |  └-ALT List(Z)
+    |  |  |  └-SEQ
+    |  |  |  |  └-ZERO
+    |  |  |  |  └-STA
+    |  |  |  |     └-a
+    |  |  |  └-SEQ List(S, C(a))
+    |  |  |     └-ONE List(S, C(a))
+    |  |  |     └-STA
+    |  |  |        └-a
+    |  |  └-ALT List(S)
+    |  |     └-ZERO
+    |  |     └-ZERO
+    |  └-STA
+    |     └-ALT
+    |        └-STA List(Z)
+    |        |  └-a
+    |        └-ALT List(S)
+    |           └-b List(Z)
+    |           └-a List(S)
+    └-SEQ List(S, Z, S, C(a), Z)
+       └-ALT List(S)
+       |  └-SEQ List(Z)
+       |  |  └-ONE List(S, C(a))
+       |  |  └-STA
+       |  |     └-a
+       |  └-ALT List(S)
+       |     └-ZERO
+       |     └-ONE List(S, C(a))
+       └-STA
           └-ALT
-             └-a List(Z)
-             └-a List(S)
+             └-STA List(Z)
+             |  └-a
+             └-ALT List(S)
+                └-b List(Z)
+                └-a List(S)
 regex after ders and then a single simp
-SEQ
- └-ALT List(S)
- |  └-SEQ List(S, C(b))
- |  |  └-STA List(S, C(a), S, C(a))
- |  |  |  └-a
- |  |  └-a List(Z)
- |  └-ONE List(S, C(b), S, C(a), Z, Z, C(a))
- └-STA
-    └-SEQ
+ALT
+ └-SEQ List(S, S, Z, C(b))
+ |  └-STA List(S, Z, S, C(a), S, C(a))
+ |  |  └-a
+ |  └-STA
+ |     └-ALT
+ |        └-STA List(Z)
+ |        |  └-a
+ |        └-ALT List(S)
+ |           └-b List(Z)
+ |           └-a List(S)
+ └-SEQ List(S, S, Z, C(b), S, Z, S, C(a), Z)
+    └-ALT List(S)
+    |  └-STA List(Z, S, C(a))
+    |  |  └-a
+    |  └-ONE List(S, S, C(a))
+    └-STA
        └-ALT
-       |  └-c List(Z)
-       |  └-b List(S)
-       └-SEQ
-          └-STA
+          └-STA List(Z)
           |  └-a
-          └-ALT
-             └-a List(Z)
+          └-ALT List(S)
+             └-b List(Z)
              └-a List(S)
 \end{verbatim}
 \end{theorem}