diff -r 0cce1aee0fb2 -r 65e786a58365 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Mon Feb 21 23:38:26 2022 +0000
+++ b/thys2/blexer2.sc	Tue Mar 01 11:14:17 2022 +0000
@@ -622,7 +622,9 @@
 
   def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
     case Nil => r
-    case c::s => bders_simp(s, bsimp(bder(c, r)))
+    case c::s => 
+      println(erase(r))
+      bders_simp(s, bsimp(bder(c, r)))
   }
   
   def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
@@ -818,59 +820,60 @@
   val pderSTAR = pderUNIV(STARREG)
 
   val refSize = pderSTAR.map(size(_)).sum
-  println("different partial derivative terms:")
-  pderSTAR.foreach(r => r match {
+  // println("different partial derivative terms:")
+  // pderSTAR.foreach(r => r match {
       
-        case SEQ(head, rstar) =>
-          println(shortRexpOutput(head) ++ "~STARREG")
-        case STAR(rstar) =>
-          println("STARREG")
+  //       case SEQ(head, rstar) =>
+  //         println(shortRexpOutput(head) ++ "~STARREG")
+  //       case STAR(rstar) =>
+  //         println("STARREG")
       
-    }
-    )
-  println("the total number of terms is")
-  //println(refSize)
-  println(pderSTAR.size)
+  //   }
+  //   )
+  // println("the total number of terms is")
+  // //println(refSize)
+  // println(pderSTAR.size)
 
   val A : Rexp= ("c" | (ONE | "b") ~ "d") ~((ONE).%)
   val B : Rexp = ((ONE).%)
   val C : Rexp = ("d") ~ ((ONE).%)
   val PRUNE_REG : Rexp = (C | B | A)
   val APRUNE_REG = internalise(PRUNE_REG)
-  // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG))
-  // println("program executes and gives: as disired!")
-  // println(shortRexpOutput(erase(program_solution)))
-  val simpedPruneReg = strongBsimp(APRUNE_REG)
-  println(shortRexpOutput(erase(simpedPruneReg)))
-  for(i <- List(100, 900 ) ){// 100, 400, 800, 840, 841, 900
-    val prog0 = "a" * i
-    //println(s"test: $prog0")
-    println(s"testing with $i a's" )
-    //val bd = bdersSimp(prog0, STARREG)//DB
-    val sbd = bdersSimpS(prog0, STARREG)//strongDB
-    starPrint(erase(sbd))
-    val subTerms = breakIntoTerms(erase(sbd))
-    //val subTermsLarge = breakIntoTerms(erase(bd))
+  // // val program_solution = pruneRexp(APRUNE_REG, breakIntoTerms(PRUNE_REG))
+  // // println("program executes and gives: as disired!")
+  // // println(shortRexpOutput(erase(program_solution)))
+  // val simpedPruneReg = strongBsimp(APRUNE_REG)
+
+  // println(shortRexpOutput(erase(simpedPruneReg)))
+  // for(i <- List(1,2 ) ){// 100, 400, 800, 840, 841, 900
+  //   val prog0 = "a" * i
+  //   //println(s"test: $prog0")
+  //   println(s"testing with $i a's" )
+  //   //val bd = bdersSimp(prog0, STARREG)//DB
+  //   val sbd = bdersSimpS(prog0, STARREG)//strongDB
+  //   starPrint(erase(sbd))
+  //   val subTerms = breakIntoTerms(erase(sbd))
+  //   //val subTermsLarge = breakIntoTerms(erase(bd))
     
-    println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}")
+  //   println(s"subterms of regex with strongDB: ${subTerms.length}")//, standard DB: ${subTermsLarge.length}")
 
 
 
-    println("the number of distinct subterms for bsimp with strongDB")
-    println(subTerms.distinct.size)
-    //println(subTermsLarge.distinct.size)
-    println("which coincides with the number of PDER terms")
+  //   println("the number of distinct subterms for bsimp with strongDB")
+  //   println(subTerms.distinct.size)
+  //   //println(subTermsLarge.distinct.size)
+  //   println("which coincides with the number of PDER terms")
 
 
-    // println(shortRexpOutput(erase(sbd)))
-    // println(shortRexpOutput(erase(bd)))
+  //   // println(shortRexpOutput(erase(sbd)))
+  //   // println(shortRexpOutput(erase(bd)))
     
-    println("pdersize, original, strongSimp")
-    println(refSize, size(STARREG),  asize(sbd))
+  //   println("pdersize, original, strongSimp")
+  //   println(refSize, size(STARREG),  asize(sbd))
 
-    val vres = strong_blexing_simp( STARREG, prog0)
-    println(vres)
-  }
+  //   val vres = strong_blexing_simp( STARREG, prog0)
+  //   println(vres)
+  // }
 //   println(vs.length)
 //   println(vs)
    
@@ -878,6 +881,9 @@
   // val prog1 = """read  n; write n"""  
   // println(s"test: $prog1")
   // println(lexing_simp(WHILE_REGS, prog1))
+  val display = ("a"| "ab").%
+  val adisplay = internalise(display)
+  bders_simp( "aaaaa".toList, adisplay)
 }
 
 small()