--- a/Spiral.scala	Wed Jan 15 13:01:10 2020 +0000
+++ b/Spiral.scala	Thu Jan 16 22:34:23 2020 +0000
@@ -558,17 +558,20 @@
   }
   def tellmewhy(){
     //val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(ALTS(List(CHAR('a'), CHAR('a'))), STAR(CHAR('a'))))) 
-    val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(CHAR('a'), STAR(CHAR('a')) ) ))
+    //val r = SEQ(ALTS(List(CHAR('a'), CHAR('b'))),ALTS(List(CHAR('a'), STAR(CHAR('a')) ) ))
+    val r = ("ab" | (  (("a")%) | "aa")  )
     //val r = ("a"|"b")~("a")
     val s = "aa"
     for(i <- 0 to s.length-1){
       val ss = s.slice(0, i+1)
-      val nangao = ders_simp(internalise(r), ss.toList)
+      val nangao = bders_simp_rf(ss.toList, internalise(r))
       val easy = (bders(ss.toList, internalise(r)))
       println(bits_print(nangao))
+      println()
       println(bits_print(easy))
       println()
-      bsimp_print(easy)
+      println(bits_print(bsimp_rf(easy)))
+      println()
     }
     println(bits_print(bsimp(bders(s.toList, internalise(r)))))
     println(bits_print(ders_simp(internalise(r), s.toList)))
@@ -591,27 +594,29 @@
     case r => r
   }
   def correctness_proof_convenient_path(){
-        val s = "abab"//rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
-        val r = ("ab"| SEQ(ONE, "ab"))//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(i <- 1 to 19999){
+        val s = rd_string_gen(alphabet_size, 3)//"abaa"//rd_string_gen(alphabet_size, 3)
+        val r = 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(internalise(r), ss.toList)
-          val easy = bsimp(bders(ss.toList, internalise(r)))
-          if(!(nangao == easy || pushbits(nangao) == (easy))){
+          val nangao = bders_simp_rf(ss.toList, r)
+          val easy = bsimp_rf(bders_rf(ss.toList, r))
+          if(!(nangao == easy)){
             println(j)
             println("not equal")
             println("string")
             println(ss)
             println("original regex")
-            println(regx_tree(r))
+            println(annotated_tree(r))
             println("regex after ders simp")
             println(annotated_tree(nangao))
             println("regex after ders")
-            println(annotated_tree(bders(ss.toList, internalise(r))))//flats' fuse when opening up AALTS causes the difference
+            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")
             println(annotated_tree(easy))
           }
         }
+      }
   }
   /*    if(bts == cdbts){//test of equality code v = retrieve internalise(r) v if |- v : r
       println(bts)
@@ -839,6 +844,8 @@
   def main(args: Array[String]) {
     //println(S.toString)
     //find_re()
+    //tellmewhy()
+    //correctness_proof_convenient_path()
     tellmewhy()
     //string_der_test()
     //comp(rd_string_gen(3,6).toList, random_struct_gen(7))