--- a/Spiral.scala	Fri Mar 15 10:46:46 2019 +0000
+++ b/Spiral.scala	Fri Mar 15 12:27:12 2019 +0000
@@ -312,7 +312,12 @@
   }
   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 ders_simp(r: ARexp, s: List[Char]): ARexp = {
+    s match {
+      case Nil => r 
+      case c::cs => ders_simp(bsimp(bder(c, r)), cs)
+    }
+  }
   def check_all(){
     for(i <- 1 to 1)
     {
@@ -322,8 +327,29 @@
         weak_sub_check(r, s, 5, size_expansion_rate)
     }
   }
+  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)
+        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(nangao != easy|| j == 2){
+            println(j)
+            if(j == 3) println("not equal")
+            println(ss)
+            println(r)
+            println(nangao)
+            println(easy)
+          }
+        }
+    }
+  }
   def main(args: Array[String]) {
-    check_all()   
+    //check_all()   
+    correctness_proof_convenient_path
   } 
 }