diff -r 3c5e58d08939 -r ff7945a988a3 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Fri May 20 18:52:03 2022 +0100
+++ b/thys2/blexer2.sc	Thu May 26 20:51:40 2022 +0100
@@ -1,3 +1,5 @@
+//Strong Bsimp to obtain Antimirov's cubic bound
+
 // A simple lexer inspired by work of Sulzmann & Lu
 //==================================================
 //
@@ -496,12 +498,37 @@
           val rs_simp = rs.map(strongBsimp5(_))
           val flat_res = flats(rs_simp)
           var dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase)
-          var dist2_res = distinctBy5(dist_res)
-          while(dist_res != dist2_res){
-            dist_res = dist2_res
-            dist2_res = distinctBy5(dist_res)
+          // var dist2_res = distinctBy5(dist_res)
+          // while(dist_res != dist2_res){
+          //   dist_res = dist2_res
+          //   dist2_res = distinctBy5(dist_res)
+          // }
+          (dist_res) match {
+            case Nil => AZERO
+            case s :: Nil => fuse(bs1, s)
+            case rs => AALTS(bs1, rs)  
           }
-          (dist2_res) match {
+    }
+    case r => r
+  }
+}
+
+def strongBsimp6(r: ARexp): ARexp =
+{
+  // println("was this called?")
+  r match {
+    case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(r2)) match {
+        case (AZERO, _) => AZERO
+        case (_, AZERO) => AZERO
+        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
+        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
+    }
+    case AALTS(bs1, rs) => {
+        // println("alts case")
+          val rs_simp = rs.map(strongBsimp6(_))
+          val flat_res = flats(rs_simp)
+          var dist_res = distinctBy6(flat_res)//distinctBy(flat_res, erase)
+          (dist_res) match {
             case Nil => AZERO
             case s :: Nil => fuse(bs1, s)
             case rs => AALTS(bs1, rs)  
@@ -688,6 +715,90 @@
   }
 }
 
+def attachCtx(r: ARexp, ctx: List[Rexp]) : List[Rexp] = {
+  val res = breakIntoTerms(oneSimp(L(erase(r), ctx))).map(oneSimp)
+  res
+}
+
+def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, inclusionPred: (C, C) => Boolean) : Boolean = {
+  inclusionPred(f(a, b), c)
+}
+def rexpListInclusion(rs1: List[Rexp], rs2: List[Rexp]) : Boolean = {
+  rs1.forall(rs2.contains)
+}
+def pAKC6(acc: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
+  // println("pakc")
+  // println(shortRexpOutput(erase(r)))
+  // println("acc")
+  // rsprint(acc)
+  // println("ctx---------")
+  // rsprint(ctx)
+  // println("ctx---------end")
+  // rsprint(breakIntoTerms(L(erase(r), ctx)).map(oneSimp))
+
+  // rprint(L(erase(r), ctx))
+  //breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(acc.contains)
+  if (ABIncludedByC(r, ctx, acc, attachCtx, rexpListInclusion)) {//acc.flatMap(breakIntoTerms
+    //println("included in acc!!!")
+    AZERO
+  }
+  else{
+    r match {
+      case ASEQ(bs, r1, r2) => 
+      (pAKC6(acc, r1, erase(r2) :: ctx)) match{
+        case AZERO => 
+          AZERO
+        case AONE(bs1) => 
+          fuse(bs1, r2)
+        case r1p => 
+          ASEQ(bs, r1p, r2)
+      }
+      case AALTS(bs, rs0) => 
+        // println("before pruning")
+        // println(s"ctx is ")
+        // ctx.foreach(r => println(shortRexpOutput(r)))
+        // println(s"rs0 is ")
+        // rs0.foreach(r => println(shortRexpOutput(erase(r))))
+        // println(s"acc is ")
+        // acc.foreach(r => println(shortRexpOutput(r)))
+        rs0.map(r => pAKC6(acc, r, ctx)).filter(_ != AZERO) match {
+          case Nil => 
+            // println("after pruning Nil")
+            AZERO
+          case r :: Nil => 
+            // println("after pruning singleton")
+            // println(shortRexpOutput(erase(r)))
+            r 
+          case rs0p => 
+          // println("after pruning non-singleton")
+            AALTS(bs, rs0p)
+        }
+      case r => r
+    }
+  }
+}
+
+
+def distinctBy6(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+  case Nil => 
+    Nil
+  case x :: xs => {
+    val erased = erase(x)
+    if(acc.contains(erased)){
+      distinctBy6(xs, acc)
+    }
+    else{
+      val pruned = pAKC6(acc, x, Nil)
+      val newTerms = breakIntoTerms(erase(pruned))
+      pruned match {
+        case AZERO => 
+          distinctBy6(xs, acc)
+        case xPrime => 
+          xPrime :: distinctBy6(xs, newTerms.map(oneSimp) ::: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
+      }
+    }
+  }
+}
 
 def breakIntoTerms(r: Rexp) : List[Rexp] = r match {
   case SEQ(r1, r2)  => breakIntoTerms(r1).map(r11 => SEQ(r11, r2))
@@ -806,7 +917,10 @@
     case Nil => r
     case c::s => bdersStrong5(s, strongBsimp5(bder(c, r)))
   }
-
+  def bdersStrong6(s: List[Char], r: ARexp) : ARexp = s match {
+    case Nil => r
+    case c::s => bdersStrong6(s, strongBsimp6(bder(c, r)))
+  }
   def bdersSimp(s: String, r: Rexp) : ARexp = bders_simp(s.toList, internalise(r))
 
   def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
@@ -1024,13 +1138,13 @@
   //val pderSTAR = pderUNIV(STARREG)
 
   //val refSize = pderSTAR.map(size(_)).sum
-  for(n <- 6 to 6){
+  for(n <- 5 to 5){
     val STARREG = n_astar(n)
     val iMax = (lcm((1 to n).toList))
-    for(i <- 1 to iMax + 50){// 100, 400, 800, 840, 841, 900 
+    for(i <- 1 to iMax + 2){// 100, 400, 800, 840, 841, 900 
       val prog0 = "a" * i
       //println(s"test: $prog0")
-      print(n)
+      print(i)
       print(" ")
       // print(i)
       // print(" ")
@@ -1089,34 +1203,17 @@
   //STAR(SEQ(ALTS(STAR(STAR(STAR(STAR(CHAR(c))))),ALTS(CHAR(c),CHAR(b))),ALTS(ZERO,SEQ(ALTS(ALTS(STAR(CHAR(c)),SEQ(CHAR(b),CHAR(a))),CHAR(c)),STAR(ALTS(ALTS(ONE,CHAR(a)),STAR(CHAR(c))))))))
   //(depth5)
   //STAR(SEQ(ALTS(ALTS(STAR(CHAR(b)),SEQ(ONE,CHAR(b))),SEQ(STAR(CHAR(a)),CHAR(b))),ALTS(ZERO,ALTS(STAR(CHAR(b)),STAR(CHAR(a))))))
-  test(rexp(4), 10000000) { (r: Rexp) => 
+  test(rexp(4), 100000) { (r: Rexp) => 
   // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
     val ss = stringsFromRexp(r)
-    val boolList = ss.map(s => {
-      val bdStrong = bdersStrong(s.toList, internalise(r))
-      val bdStrong5 = bdersStrong5(s.toList, internalise(r))
-      val bdFurther5 = strongBsimp5(bdStrong5)
-      val sizeFurther5 = asize(bdFurther5)
-      val pdersSet = pderUNIV(r)
-      val size5 = asize(bdStrong5)
-      val size0 = asize(bdStrong)
+    val boolList = ss.filter(s => s != "").map(s => {
+      //val bdStrong = bdersStrong(s.toList, internalise(r))
+      val bdStrong6 = bdersStrong6(s.toList, internalise(r))
+      val bdStrong6Set = breakIntoTerms(erase(bdStrong6))
+      val pdersSet = pderUNIV(r).flatMap(r => breakIntoTerms(r))
       // println(s)
-      // println("pdersSet size")
-      // println(pdersSet.size)
-      // pdersSet.foreach(r => println(shortRexpOutput(r)))
-      // println("after bdStrong5")
-      
-      // println(shortRexpOutput(erase(bdStrong5)))
-      // println(breakIntoTerms(erase(bdStrong5)).size)
-      
-      // println("after bdStrong")
-      // println(shortRexpOutput(erase(bdStrong)))
-      // println(breakIntoTerms(erase(bdStrong)).size)
-      // println(size5, size0, sizeFurther5)
-      // aprint(strongBsimp5(bdStrong))
-      // println(asize(strongBsimp5(bdStrong5)))
-      // println(s)
-      size5 <= size0 
+      // println(bdStrong6Set.size, pdersSet.size)
+      bdStrong6Set.size <= pdersSet.size
     })
     // println(boolList)
     //!boolList.exists(b => b == false)
@@ -1125,11 +1222,40 @@
 
 
 }
-small()
-// generator_test()
+// small()
+generator_test()
 
+def counterexample_check() {
+  val r = STAR(SEQ(ALTS(ALTS(CHAR('b'),CHAR('c')),
+    SEQ(CHAR('b'),CHAR('b'))),ALTS(SEQ(ONE,CHAR('b')),CHAR('a'))))
+  val s = "bbbb"
+  val bdStrong5 = bdersStrong6(s.toList, internalise(r))
+  val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
+  val pdersSet = pderUNIV(r)//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+  println("original regex ")
+  rprint(r)
+  println("after strong bsimp")
+  aprint(bdStrong5)
+  println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   ")
+  rsprint(bdStrong5Set)
+  println("after pderUNIV")
+  rsprint(pdersSet.toList)
+}
+// counterexample_check()
 // 1
-
+def newStrong_test() {
+  val r2 = (CHAR('b') | ONE)
+  val r0 = CHAR('d')
+  val r1 = (ONE | CHAR('c'))
+  val expRexp = (SEQ(r2, r0) | SEQ(SEQ(r1, r2), r0))
+  println(s"original regex is: ")
+  rprint(expRexp)
+  val expSimp5 = strongBsimp5(internalise(expRexp))
+  val expSimp6 = strongBsimp6(internalise(expRexp))
+  aprint(expSimp5)
+  aprint(expSimp6)
+}
+// newStrong_test()
 // 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'))),