diff -r 7a349fe58bf4 -r 622ddbb1223a Spiral.scala
--- a/Spiral.scala	Fri Mar 15 12:27:12 2019 +0000
+++ b/Spiral.scala	Sat Mar 16 14:14:42 2019 +0000
@@ -29,6 +29,35 @@
   val alphabet = ("""abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ0123456789.:"=()\;-+*!<>\/%{} """+"\n\t").toSet//Set('a','b','c')
   def bregx_tree(r: BRexp): Element = regx_tree(berase(r))
   def regx_tree(r: Rexp): Element = aregx_tree(internalise(r))
+  def annotated_tree(r: ARexp): Element = {
+    r match {
+      case ACHAR(bs, d) => {
+        //val Some(d) = alphabet.find(f)
+        d match {
+          case '\n' => elem("\\n")
+          case '\t' => elem("\\t")
+          case ' ' => elem("space")
+          case d => elem(d.toString)
+        }   
+      }
+      case AONE(bs) => {
+        elem("ONE")
+      }
+      case AZERO => {
+        elem("ZERO")
+      }
+      case ASEQ(bs, r1, r2) => {
+        binary_print("SEQ", r1, r2)
+      }
+      case AALTS(bs, rs) => {
+        //elem("Awaiting completion")
+        list_print("ALT", rs)
+      }
+      case ASTAR(bs, r) => {
+        list_print("STA", List(r))
+      }
+    } 
+  }
   def aregx_tree(r: ARexp): Element = {
     r match {
       case ACHAR(bs, d) => {
@@ -276,11 +305,11 @@
     //this is for comparison between normal simp and the weakened version of simp
     //normal simp will be performed on syncold
     //weakend simp will be performed on old
-    var syncold = brternalise(r)
+    var syncold = internalise(r)
     val all_chars = s.toList
     for (i <- 0 to s.length - 1){
-      val syncder_res = brder(all_chars(i), syncold)
-      val syncsimp_res = strong_br_simp(syncder_res)
+      val syncder_res = bder(all_chars(i), syncold)
+      val syncsimp_res = super_bsimp(syncder_res)
       //see brder for detailed explanation
       //just changes bit Z to S when deriving an ALTS, 
       //signifying that the structure has been "touched" and
@@ -289,10 +318,14 @@
       val simp_res = br_simp(der_res)
       val anatomy = bspill(simp_res)
       //track if the number of regular expressions exceeds those in the PD set(remember PD means the pders over A*)
-      if(f(anatomy, pd)  == false || i == 1){
-        println(size(berase(syncsimp_res)))
+      if(f(List(berase(simp_res)), pd)  == false ){
+        println(size(erase(syncsimp_res)))
         println(size(berase(simp_res)))
         println(bregx_tree(simp_res))
+        println(s)
+        println(i)
+        println(r)
+        println()
         println(anatomy.map(size).sum)
         println(pd.map(size).sum)
       }  
@@ -311,22 +344,22 @@
     }
   }
   def size_comp(anatomy: List[Rexp], pd: Set[Rexp]):Boolean = {println("size of PD and bspilled simp regx: ", pd.size, anatomy.size); true}
-  def size_expansion_rate(anatomy: List[Rexp], pd: Set[Rexp]): Boolean = if(anatomy.size > (pd.size)*2 ) {println("size of PD and bspilled simp regx: ", pd.size, anatomy.size); inclusion_truth(anatomy, pd); false }else {true}
+  def size_expansion_rate(r: List[Rexp], pd: Set[Rexp]): Boolean = if(size(r(0)) > (pd.map(size).sum) * 3 ) { false }else {true}
   def ders_simp(r: ARexp, s: List[Char]): ARexp = {
     s match {
       case Nil => r 
       case c::cs => ders_simp(bsimp(bder(c, r)), cs)
     }
   }
+  val big_panda = STAR(STAR(STAR(ALTS(List(ALTS(List(CHAR('c'), CHAR('b'))), SEQ(CHAR('c'),CHAR('c')))))))
+  val str_panda = "ccccb"
   def check_all(){
-    for(i <- 1 to 1)
-    {
-        val s = "bb"//rd_string_gen(alphabet_size, 5)//"ac"//rd_string_gen(alphabet_size, 5)
-        val r = STAR(STAR(ALTS(List(SEQ(CHAR('b'),CHAR('b')), ALTS(List(CHAR('a'), CHAR('b')))))))//balanced_struct_gen(4)//SEQ(ALTS(List(STAR("a"),ALTS(List("a","c")))),SEQ(ALTS(List("c","a")),ALTS(List("c","b")))) //random_struct_gen(7)
-        //subset_check(r, s)
-        weak_sub_check(r, s, 5, size_expansion_rate)
-    }
+
+        weak_sub_check(big_panda, str_panda, 6, size_expansion_rate)
+
   }
+  //simplified regex size 291, so called pd_simp size 70 (did not do simplification to terms in the PD set)
+
   def correctness_proof_convenient_path(){
     for(i <- 1 to 1)
     {
@@ -336,12 +369,18 @@
           val ss = s.slice(0, j+ 1)
           val nangao = ders_simp(r, ss.toList)
           val easy = bsimp(bders(ss.toList, r))
-          if(nangao != easy|| j == 2){
+          if(true){
             println(j)
             if(j == 3) println("not equal")
+            println("string")
             println(ss)
+            println("original regex")
             println(r)
+            println("regex after ders simp")
             println(nangao)
+            println("regex after ders")
+            println(bders(ss.toList, r))
+            println("regex after ders and then a single simp")
             println(easy)
           }
         }
@@ -349,7 +388,8 @@
   }
   def main(args: Array[String]) {
     //check_all()   
-    correctness_proof_convenient_path
+    enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
+    //correctness_proof_convenient_path()
   } 
 }