diff -r 47c75ba5ad28 -r 994403dbbed5 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Fri Feb 11 17:28:41 2022 +0000
+++ b/thys2/blexer2.sc	Wed Feb 16 17:20:40 2022 +0000
@@ -478,7 +478,7 @@
     r match {
       case ASEQ(bs, r1, r2) => 
         val termsTruncated = allowableTerms.collect(rt => rt match {
-          case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p
+          case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2)) 
         })
         val pruned : ARexp = pruneRexp(r1, termsTruncated)
         pruned match {
@@ -489,7 +489,10 @@
 
       case AALTS(bs, rs) => 
         //allowableTerms.foreach(a => println(shortRexpOutput(a)))        
-        val rsp = rs.map(r => pruneRexp(r, allowableTerms)).filter(r => r != AZERO)
+        val rsp = rs.map(r => 
+                      pruneRexp(r, allowableTerms)
+                    )
+                    .filter(r => r != AZERO)
         rsp match {
           case Nil => AZERO
           case r1::Nil => fuse(bs, r1)
@@ -509,15 +512,17 @@
 
 
   def distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+    
     case Nil => Nil
     case x :: xs =>
+      //assert(acc.distinct == acc)
       val erased = erase(x)
       if(acc.contains(erased))
         distinctBy4(xs, acc)
       else{
         val addToAcc =  breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
-        val xp = pruneRexp(x, addToAcc)
-        xp match {
+        //val xp = pruneRexp(x, addToAcc)
+        pruneRexp(x, addToAcc) match {
           case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
           case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
         }
@@ -827,40 +832,41 @@
   //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 = (A | B | C)
-  // val APRUNE_REG = internalise(PRUNE_REG)
+  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)))
-  
-  for(i <- List( 4, 8, 9, 17, 29) ){// 100, 400, 800, 840, 841, 900
+  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 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 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 and standardDB")
+    println("the number of distinct subterms for bsimp with strongDB")
     println(subTerms.distinct.size)
-    println(subTermsLarge.distinct.size)
+    //println(subTermsLarge.distinct.size)
     println("which coincides with the number of PDER terms")
 
 
     // println(shortRexpOutput(erase(sbd)))
     // println(shortRexpOutput(erase(bd)))
     
-    println("pdersize, original, strongSimp, bsimp")
-    println(refSize, size(STARREG),  asize(sbd), asize(bd))
+    println("pdersize, original, strongSimp")
+    println(refSize, size(STARREG),  asize(sbd))
 
     val vres = strong_blexing_simp( STARREG, prog0)
     println(vres)