--- a/Spiral.scala	Sat Mar 16 15:00:43 2019 +0000
+++ b/Spiral.scala	Sat Mar 16 20:05:13 2019 +0000
@@ -37,24 +37,24 @@
           case '\n' => elem("\\n")
           case '\t' => elem("\\t")
           case ' ' => elem("space")
-          case d => elem(d.toString)
+          case d => if(bs.isEmpty)  elem(d.toString) else elem(d.toString++" ") beside elem(bs.toString)
         }   
       }
       case AONE(bs) => {
-        elem("ONE")
+        if(bs.isEmpty)  elem("ONE") else elem("ONE ") beside elem(bs.toString)
       }
       case AZERO => {
-        elem("ZERO")
+        elem("ZERO") 
       }
       case ASEQ(bs, r1, r2) => {
-        binary_print("SEQ", r1, r2)
+        annotated_binary_print("SEQ", r1, r2, bs)
       }
       case AALTS(bs, rs) => {
         //elem("Awaiting completion")
-        list_print("ALT", rs)
+        annotated_list_print("ALT", rs, bs)  
       }
       case ASTAR(bs, r) => {
-        list_print("STA", List(r))
+        annotated_list_print("STA", List(r), bs)
       }
     } 
   }
@@ -111,6 +111,58 @@
       }
     }
   }
+    def annotated_list_print(name: String, rs: List[ARexp], bs: List[Bit]): Element = {
+    rs match {
+      case r::Nil => {
+        val pref = annotated_tree(r)
+        val head = if(bs.isEmpty) elem(name) else elem(name ++ " ") beside elem(bs.toString)
+        (head left_align (port up_align pref) ) 
+      }
+      case r2::r1::Nil => {
+        annotated_binary_print(name, r2, r1, bs)
+      }
+      case r::rs1 => {
+        val pref = annotated_tree(r)
+        val head = if (bs.isEmpty) elem(name) else elem(name ++ " ") beside elem(bs.toString)
+        if (pref.height > 1){
+          val link = elem('|', 1, pref.height - 1)
+          (head left_align ((port above link) beside pref)) left_align annotated_tail_print(rs1)    
+        }
+        else{
+          (head left_align (port beside pref) ) left_align annotated_tail_print(rs1)
+        }
+      }
+    }
+  }
+
+  def annotated_tail_print(rs: List[ARexp]): Element = {
+    rs match {
+      case r2::r1::Nil => {
+        val pref = annotated_tree(r2)
+        val suff = annotated_tree(r1)
+        if (pref.height > 1){
+          val link = elem('|', 1, pref.height - 1)
+          ((port above link) beside pref) left_align (port up_align suff)
+        }
+        else{
+          (port beside pref) left_align (port up_align suff)
+        } 
+      }
+      case r2::rs1 => {
+        val pref = annotated_tree(r2)
+        
+        if (pref.height > 1){
+          val link = elem('|', 1, pref.height - 1)
+          ((port above link) beside pref) left_align annotated_tail_print(rs1)//(port up_align tail_print(rs1) )
+        }
+        else{
+          (port beside pref) left_align annotated_tail_print(rs1)//(port up_align tail_print(rs1))
+        } 
+        //pref left_align tail_print(rs1)
+      }
+    }
+  }
+
   def tail_print(rs: List[ARexp]): Element = {
     rs match {
       case r2::r1::Nil => {
@@ -142,7 +194,7 @@
   def binary_print(name: String, r1: ARexp, r2: ARexp): Element = {
     val pref = aregx_tree(r1)
     val suff = aregx_tree(r2)
-    val head = elem(name)
+    val head = elem(name) 
     if (pref.height > 1){
       val link = elem('|', 1, pref.height - 1)
       (head left_align ((port above link) beside pref) ) left_align (port up_align suff)
@@ -151,6 +203,19 @@
       (head left_align (port beside pref) ) left_align (port up_align suff)
     }
   }
+  def annotated_binary_print(name: String, r1: ARexp, r2: ARexp, bs: List[Bit]): Element = {
+    val pref = annotated_tree(r1)
+    val suff = annotated_tree(r2)
+    val head = if (bs.isEmpty) elem(name) else elem(name ++ " ") beside elem(bs.toString)
+    if (pref.height > 1){
+      val link = elem('|', 1, pref.height - 1)
+      (head left_align ((port above link) beside pref) ) left_align (port up_align suff)
+    }
+    else{
+      (head left_align (port beside pref) ) left_align (port up_align suff)
+    }
+  }
+
   val arr_of_size = ListBuffer.empty[Int]
 
   def pC(r: Rexp): Set[Rexp] = {//PD's companion
@@ -335,7 +400,6 @@
         println(s)
         println(i)
         println(r)
-        println()
         println(anatomy.map(size).sum)
         println(pd.map(size).sum)
       }  
@@ -389,19 +453,21 @@
             println("regex after ders simp")
             println(nangao)
             println("regex after ders")
-            println(bders(ss.toList, r))
+            println(annotated_tree(bders(ss.toList, r)))
             println("regex after ders and then a single simp")
-            println(easy)
+            println(annotated_tree(easy))
           }
         }
     }
   }
+  def radical_correctness(){
+    enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
+    random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
+  }
   def main(args: Array[String]) {
     //check_all()   
-    //enum(3, "abc").map(tests_blexer_simp(strs(3, "abc"))).toSet
-    //
-    random_pool(1, 5).map(tests_blexer_simp(strs(5, "abc"))).toSet
-    //correctness_proof_convenient_path()
+    //radical_correctness()
+    correctness_proof_convenient_path()
   } 
 }