diff -r 84938708781d -r 6fecb7fe8cd0 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Tue May 17 01:44:30 2022 +0100
+++ b/thys2/blexer2.sc	Fri May 20 18:48:34 2022 +0100
@@ -983,96 +983,60 @@
             starPrint(r2)
             println(")")
           case ZERO => println("0")
-        
       }
 
 // @arg(doc = "small tests")
-val STARREG = //((( (STAR("aa")) | STAR("aaa") ).%).%)
+def n_astar_list(d: Int) : Rexp = {
+  if(d == 0) STAR("a") 
+  else ALTS(STAR("a" * d), n_astar_list(d - 1))
+}
+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_aux(d: Int) = {
+  if(d == 0) n_astar_alts(0)
+  else ALTS(n_astar_alts(d), n_astar_alts(d - 1))
+}
+
+def n_astar(d: Int) : Rexp = STAR(n_astar_aux(d))
+//val STARREG = n_astar(3)
+// ( STAR("a") | 
+//                  ("a" | "aa").% | 
+//                 ( "a" | "aa" | "aaa").% 
+//                 ).%
+                //( "a" | "aa" | "aaa" | "aaaa").% |
+                //( "a" | "aa" | "aaa" | "aaaa" | "aaaaa").% 
 (((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).%
 
 // @main
 
-
+def lcm(list: Seq[Int]):Int=list.foldLeft(1:Int){
+  (a, b) => b * a /
+  Stream.iterate((a,b)){case (x,y) => (y, x%y)}.dropWhile(_._2 != 0).head._1.abs
+}
 
 def small() = {
-
-
-//   println(lexing_simp(NOTREG, prog0))
-//   val v = lex_simp(NOTREG, prog0.toList)
-//   println(v)
-
-//   val d =  (lex_simp(NOTREG, prog0.toList))
-//   println(d)
-  val pderSTAR = pderUNIV(STARREG)
-
-  val refSize = pderSTAR.map(size(_)).sum
-  // println("different partial derivative terms:")
-  // pderSTAR.foreach(r => r match {
-      
-  //       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)
-
-  // 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)))
-
+  //val pderSTAR = pderUNIV(STARREG)
 
-  for(i <- List(1,2,3,4,10, 100, 400, 841, 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 = bdersStrongRexp(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("the number of distinct subterms for bsimp with strongDB")
-    println(subTerms.distinct.size)
-    //println(subTermsLarge.distinct.size)
-    if(pderSTAR.size > subTerms.length)
-      println(s"which is less than or equal to the number of PDER terms: ${pderSTAR.size}")
-
-
-    // println(shortRexpOutput(erase(sbd)))
-    // println(shortRexpOutput(erase(bd)))
-    
-    println("pdersize, original, strongSimp")
-    println(refSize, size(STARREG),  asize(sbd))
-
-    //val vres = strong_blexing_simp( STARREG, prog0)
-    //println(vres)
+  //val refSize = pderSTAR.map(size(_)).sum
+  for(n <- 6 to 6){
+    val STARREG = n_astar(n)
+    val iMax = (lcm((1 to n).toList))
+    for(i <- 1 to iMax + 50){// 100, 400, 800, 840, 841, 900 
+      val prog0 = "a" * i
+      //println(s"test: $prog0")
+      print(n)
+      print(" ")
+      // print(i)
+      // print(" ")
+      println(asize(bders_simp(prog0.toList, internalise(STARREG))))
+    }
   }
-  // println(vs.length)
-  // println(vs)
-   
-
-  // 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)
 }
 
 def generator_test() {
@@ -1161,15 +1125,15 @@
 
 
 }
-// small()
-generator_test()
+small()
+// generator_test()
 
-1
+// 1
 
-SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
-SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
-STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),
-SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
+// SEQ(SEQ(SEQ(ONE,CHAR('b')),STAR(CHAR('b'))),
+// SEQ(ALTS(ALTS(ZERO,STAR(CHAR('b'))),
+// STAR(ALTS(CHAR('a'),SEQ(SEQ(STAR(ALTS(STAR(CHAR('c')),CHAR('a'))),
+// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
 
 
 // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))