diff -r cc54ce075db5 -r 6acbc939af6a thys2/blexer2.sc
--- a/thys2/blexer2.sc	Fri Jun 03 16:45:30 2022 +0100
+++ b/thys2/blexer2.sc	Mon Jun 06 03:05:31 2022 +0100
@@ -542,19 +542,33 @@
 }
 
 def distinctWith(rs: List[ARexp], 
-                f: (ARexp, Set[Rexp]) => ARexp, 
+                pruneFunction: (ARexp, Set[Rexp]) => ARexp, 
                 acc: Set[Rexp] = Set()) : List[ARexp] = 
   rs match{
     case Nil => Nil
     case r :: rs => 
       if(acc(erase(r)))
-        distinctWith(rs, f, acc)
+        distinctWith(rs, pruneFunction, acc)
       else {
-        val pruned_r = f(r, acc)
-        pruned_r :: distinctWith(rs, f, strongBreakIntoTerms(erase(pruned_r)) ++: acc)
+        val pruned_r = pruneFunction(r, acc)
+        pruned_r :: 
+        distinctWith(rs, 
+          pruneFunction, 
+          turnIntoTerms(erase(pruned_r)) ++: acc
+        )
       }
   }
 
+// def distinctByPlus(rs: List[ARexp], acc: Set[Rexp] = Set()) : 
+// List[ARexp] =  rs match {
+//   case Nil => Nil
+//   case r :: rs =>
+//     if(acc.contains(erase(r)))
+//       distinctByPlus(rs, acc)
+//     else 
+//       prune(r, acc) :: distinctByPlus(rs, prune(r, acc) +: acc)
+// }
+
 //r = r' ~ tail => returns r'
 def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = r match {
   case SEQ(r1, r2) => 
@@ -805,19 +819,18 @@
 
 }
 
-def strongBreakIntoTerms(r: Rexp): List[Rexp] = r match {
+def turnIntoTerms(r: Rexp): List[Rexp] = r match {
   case SEQ(r1, r2)  => if(isOne(r1)) 
-                          //strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2)) ::: 
-                          strongBreakIntoTerms(r2) 
+                          turnIntoTerms(r2) 
                        else 
-                          strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2))
-  case ALTS(r1, r2) => strongBreakIntoTerms(r1) ::: strongBreakIntoTerms(r2)
+                          turnIntoTerms(r1).map(r11 => SEQ(r11, r2))
+  case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
   case ZERO => Nil
   case _ => r :: Nil
 }
 
 def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
-  val res = strongBreakIntoTerms((L(erase(r), ctx))).map(oneSimp)
+  val res = turnIntoTerms((L(erase(r), ctx))).map(oneSimp)
   res.toSet
 }
 
@@ -868,7 +881,7 @@
     }
     else{
       val pruned = prune6(acc, x, Nil)
-      val newTerms = strongBreakIntoTerms(erase(pruned))
+      val newTerms = turnIntoTerms(erase(pruned))
       pruned match {
         case AZERO => 
           distinctBy6(xs, acc)
@@ -1201,11 +1214,11 @@
 def n_astar_alts(d: Int) : Rexp = d match {
   case 0 => n_astar_list(0)
   case d => STAR(n_astar_list(d))
-  // case r1 :: r2 :: Nil => ALTS(r1, r2)
-  // case r1 :: Nil => r1
-  // case r :: rs => ALTS(r, n_astar_alts(rs))
-  // case Nil => throw new Error("should give at least 1 elem")
-}
+  }
+def n_astar_alts2(d: Int) : Rexp = d match {
+  case 0 => n_astar_list(0)
+  case d => STAR(STAR(n_astar_list(d)))
+  }
 def n_astar_aux(d: Int) = {
   if(d == 0) n_astar_alts(0)
   else ALTS(n_astar_alts(d), n_astar_alts(d - 1))
@@ -1233,9 +1246,9 @@
 
   //val refSize = pderSTAR.map(size(_)).sum
   for(n <- 5 to 5){
-    val STARREG = n_astar(n)
+    val STARREG = n_astar_alts2(n)
     val iMax = (lcm((1 to n).toList))
-    for(i <- 1 to iMax + 2){// 100, 400, 800, 840, 841, 900 
+    for(i <- 0 to iMax ){// 100, 400, 800, 840, 841, 900 
       val prog0 = "a" * i
       //println(s"test: $prog0")
       print(i)
@@ -1243,10 +1256,11 @@
       // print(i)
       // print(" ")
       println(asize(bders_simp(prog0.toList, internalise(STARREG))))
+      // println(asize(bdersStrong7(prog0.toList, internalise(STARREG))))
     }
   }
 }
-
+small()
 def generator_test() {
 
   test(rexp(4), 1000000) { (r: Rexp) => 
@@ -1255,9 +1269,9 @@
     val boolList = ss.filter(s => s != "").map(s => {
       //val bdStrong = bdersStrong(s.toList, internalise(r))
       val bdStrong6 = bdersStrong7(s.toList, internalise(r))
-      val bdStrong6Set = strongBreakIntoTerms(erase(bdStrong6))
-      val pdersSet = pderUNIV(r)//.flatMap(r => strongBreakIntoTerms(r))
-      val pdersSetBroken = pdersSet.flatMap(r => strongBreakIntoTerms(r))
+      val bdStrong6Set = turnIntoTerms(erase(bdStrong6))
+      val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
+      val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
       bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size
     })
     //println(boolList)
@@ -1280,7 +1294,7 @@
   val s = "b"
   val bdStrong5 = bdersStrong7(s.toList, internalise(r))
   val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
-  val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => strongBreakIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+  val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
   println("original regex ")
   rprint(r)
   println("after strong bsimp")
@@ -1291,7 +1305,7 @@
   rsprint(pdersSet.toList)
 
 }
-counterexample_check()
+// counterexample_check()
 
 def linform_test() {
   val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) //