diff -r ab626b60ee64 -r 4d9eecfc936a thys2/blexer2.sc
--- a/thys2/blexer2.sc	Sun May 01 11:50:46 2022 +0100
+++ b/thys2/blexer2.sc	Mon May 02 00:23:39 2022 +0100
@@ -137,7 +137,7 @@
   if(len <= 0) single(Nil)
   else{
     for { 
-      c <- chars_range('a', 'd')
+      c <- chars_range('a', 'c')
       tail <- char_list(len - 1)
     } yield c :: tail
   }
@@ -492,17 +492,18 @@
     case AALTS(bs1, rs) => {
         // println("alts case")
           val rs_simp = rs.map(strongBsimp5(_))
-
           val flat_res = flats(rs_simp)
-
-          val dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase)
-
-          dist_res match {
+          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)
+          }
+          (dist2_res) match {
             case Nil => AZERO
             case s :: Nil => fuse(bs1, s)
             case rs => AALTS(bs1, rs)  
           }
-        
     }
     case r => r
   }
@@ -604,20 +605,34 @@
 def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
   case Nil => acc
   case r :: rs1 => 
-    if(acc == ONE) 
-      L(r, rs1) 
-    else
+    // if(acc == ONE) 
+    //   L(r, rs1) 
+    // else
       L(SEQ(acc, r), rs1)
 }
 
-def pAKC(rs: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
-  if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(rs.contains)) {//rs.flatMap(breakIntoTerms
+def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
+def rsprint(rs: List[Rexp]) = rs.foreach(r => println(shortRexpOutput(r)))
+def aprint(a: ARexp) = println(shortRexpOutput(erase(a)))
+def asprint(as: List[ARexp]) = as.foreach(a => println(shortRexpOutput(erase(a))))
+
+def pAKC(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))
+
+  if (breakIntoTerms(L(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
     AZERO
   }
   else{
     r match {
       case ASEQ(bs, r1, r2) => 
-      (pAKC(rs, r1, erase(r2) :: ctx)) match{
+      (pAKC(acc, r1, erase(r2) :: ctx)) match{
         case AZERO => 
           AZERO
         case AONE(bs1) => 
@@ -631,9 +646,9 @@
         // ctx.foreach(r => println(shortRexpOutput(r)))
         // println(s"rs0 is ")
         // rs0.foreach(r => println(shortRexpOutput(erase(r))))
-        // println(s"rs is ")
-        // rs.foreach(r => println(shortRexpOutput(r)))
-        rs0.map(r => pAKC(rs, r, ctx)).filter(_ != AZERO) match {
+        // println(s"acc is ")
+        // acc.foreach(r => println(shortRexpOutput(r)))
+        rs0.map(r => pAKC(acc, r, ctx)).filter(_ != AZERO) match {
           case Nil => 
             // println("after pruning Nil")
             AZERO
@@ -1091,22 +1106,54 @@
   //   })
   //   !boolList.exists(b => b == false)
   // }
-  //test(rexp(3), 10000000) { (r: Rexp) => 
-  test(single(STAR(SEQ(SEQ(ALTS(CHAR('b'),STAR(CHAR('b'))),CHAR('b')),ALTS(ALTS(STAR(CHAR('c')),SEQ(CHAR('a'),CHAR('c'))),ALTS(ZERO,ONE))))), 1) {(r: Rexp) =>
+  //*** example where bdStrong5 has a smaller size than bdStrong
+  // test(single(STAR(SEQ(ALTS(SEQ(STAR(CHAR('a')),ALTS(ALTS(ONE,ZERO),SEQ(ONE,ONE))),CHAR('a')),ONE))), 1) { (r: Rexp) => 
+  //*** depth 5 example bdStrong5 larger size than bdStrong
+  // test(single(STAR(SEQ(SEQ(ALTS(CHAR('b'),STAR(CHAR('b'))),CHAR('b')),(ALTS(STAR(CHAR('c')), ONE))))), 1) {(r: Rexp) =>
+ 
+ 
+ 
+  //sanity check from Christian's request
+  // val r = ("a" | "ab") ~ ("bc" | "c")
+  // val a = internalise(r)
+  // val aval = blexing_simp(r, "abc")
+  // println(aval)
+
+  //sample counterexample:(depth 7)
+  //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) => 
+  // 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)
-      println(s)
-      println(shortRexpOutput(erase(bdStrong5)))
-      println(shortRexpOutput(erase(bdStrong)))
-      println(size5, size0)
       // println(s)
-      size5 <= size0
+      // 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(boolList)
+    //!boolList.exists(b => b == false)
     !boolList.exists(b => b == false)
   }