diff -r 2c02d27ec0a3 -r 2b95bcd2ac73 Spiral.scala
--- a/Spiral.scala	Fri Mar 22 12:53:56 2019 +0000
+++ b/Spiral.scala	Sat Mar 23 11:53:09 2019 +0000
@@ -433,25 +433,28 @@
 
   }
   //simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set)
-
+  def pushbits(r: ARexp): ARexp = r match {
+    case AALTS(bs, rs) => AALTS(Nil, rs.map(fuse(bs, _)))
+    case r => r
+  }
   def correctness_proof_convenient_path(){
     for(i <- 1 to 1)
     {
-        val s = "abaa"//rd_string_gen(alphabet_size, 3)
-        val r = ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
+        val s = "baa"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+        val 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'))))))//internalise(random_struct_gen(4))//ASTAR(List(),AALTS(List(),List(ASTAR(List(Z),ACHAR(List(),'a')), ASEQ(List(S),ACHAR(List(),'a'),ACHAR(List(),'b')))))//internalise(balanced_struct_gen(3))//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
         for(j <- 0 to s.length - 1){
           val ss = s.slice(0, j+ 1)
           val nangao = ders_simp(r, ss.toList)
           val easy = bsimp(bders(ss.toList, r))
-          if(true){
+          if(!(nangao == easy || pushbits(nangao) == (easy))){
             println(j)
-            if(j == 3) println("not equal")
+            println("not equal")
             println("string")
             println(ss)
             println("original regex")
-            println(r)
+            println(annotated_tree(r))
             println("regex after ders simp")
-            println(nangao)
+            println(annotated_tree(nangao))
             println("regex after ders")
             println(annotated_tree(bders(ss.toList, r)))//flats' fuse when opening up AALTS causes the difference
             println("regex after ders and then a single simp")