--- a/thys2/blexer1.sc	Wed Feb 02 22:30:41 2022 +0000
+++ b/thys2/blexer1.sc	Fri Feb 04 00:05:12 2022 +0000
@@ -361,7 +361,7 @@
       case AALTS(bs1, rs) => {
             val rs_simp = rs.map(bsimp(_))
             val flat_res = flats(rs_simp)
-            val dist_res = strongDistinctBy(flat_res)//distinctBy(flat_res, erase)
+            val dist_res = distinctBy(flat_res, erase)//strongDB(flat_res)//distinctBy(flat_res, erase)
             dist_res match {
               case Nil => AZERO
               case s :: Nil => fuse(bs1, s)
@@ -372,6 +372,30 @@
       case r => r
     }
   }
+  def strongBsimp(r: ARexp): ARexp =
+  {
+    r match {
+      case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(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) => {
+            val rs_simp = rs.map(strongBsimp(_))
+            val flat_res = flats(rs_simp)
+            val dist_res = strongDB(flat_res)//distinctBy(flat_res, erase)
+            dist_res match {
+              case Nil => AZERO
+              case s :: Nil => fuse(bs1, s)
+              case rs => AALTS(bs1, rs)  
+            }
+          
+      }
+      case r => r
+    }
+  }
+
   def bders (s: List[Char], r: ARexp) : ARexp = s match {
     case Nil => r
     case c::s => bders(s, bder(c, r))
@@ -487,13 +511,13 @@
   } 
 
 
-  def strongDistinctBy(xs: List[ARexp], 
+  def strongDB(xs: List[ARexp], 
                        acc1: List[Rexp] = Nil, 
                        acc2 : List[(List[Rexp], Rexp)] = Nil): List[ARexp] = xs match {
     case Nil => Nil
     case (x::xs) => 
         if(acc1.contains(erase(x)))
-            strongDistinctBy(xs, acc1, acc2)
+            strongDB(xs, acc1, acc2)
         else{
             x match {
                 case ASTAR(bs0, r0) => 
@@ -502,7 +526,7 @@
                         r2stl => {val (r2s, tl) = r2stl; tl == erase(r0) } 
                     )
                     if(i == -1){ 
-                        x::strongDistinctBy(
+                        x::strongDB(
                             xs, erase(x)::acc1, (ONE::Nil, erase(r0))::acc2
                         )
                     }
@@ -513,10 +537,10 @@
                         newHeads match{
                             case newHead::Nil =>
                                 ASTAR(bs0, r0) :: 
-                                strongDistinctBy(xs, erase(x)::acc1, 
+                                strongDB(xs, erase(x)::acc1, 
                                 acc2.updated(i, (oldHeadsUpdated, headListAlready._2)) )//TODO: acc2 already contains headListAlready
                             case Nil =>
-                                strongDistinctBy(xs, erase(x)::acc1, 
+                                strongDB(xs, erase(x)::acc1, 
                                 acc2)
                         }
                     }                
@@ -526,7 +550,7 @@
                         r2stl => {val (r2s, tl) = r2stl; tl == erase(r0) } 
                     )
                     if(i == -1){ 
-                        x::strongDistinctBy(
+                        x::strongDB(
                             xs, erase(x)::acc1, (headList.map(erase(_)), erase(r0))::acc2
                         )
                     }
@@ -537,18 +561,18 @@
                         newHeads match{
                             case newHead::Nil =>
                                 ASEQ(bs, newHead, ASTAR(bs0, r0)) :: 
-                                strongDistinctBy(xs, erase(x)::acc1, 
+                                strongDB(xs, erase(x)::acc1, 
                                 acc2.updated(i, (oldHeadsUpdated, headListAlready._2)) )//TODO: acc2 already contains headListAlready
                             case Nil =>
-                                strongDistinctBy(xs, erase(x)::acc1, 
+                                strongDB(xs, erase(x)::acc1, 
                                 acc2)
                             case hds => val AALTS(bsp, rsp) = r1
                                 ASEQ(bs, AALTS(bsp, hds), ASTAR(bs0, r0)) ::
-                                strongDistinctBy(xs, erase(x)::acc1,
+                                strongDB(xs, erase(x)::acc1,
                                 acc2.updated(i, (oldHeadsUpdated, headListAlready._2)))
                         }
                     }
-                case rPrime => x::strongDistinctBy(xs, erase(x)::acc1, acc2)    
+                case rPrime => x::strongDB(xs, erase(x)::acc1, acc2)    
             }
                 
         }
@@ -586,12 +610,12 @@
 
 
 // @arg(doc = "small tests")
-val STARREG = ("a" | "aa").%
+val STARREG = ((STAR("a") | STAR("aa") ).%).%
 
 @main
 def small() = {
 
-  val prog0 = """aaa"""
+  val prog0 = """aaaaaaaaa"""
   println(s"test: $prog0")
 //   println(lexing_simp(NOTREG, prog0))
 //   val v = lex_simp(NOTREG, prog0.toList)