diff -r 3a1fd5ea2484 -r 5bf9f94c02e1 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Thu Jun 09 22:08:06 2022 +0100
+++ b/thys2/blexer2.sc	Sun Jun 12 17:03:09 2022 +0100
@@ -915,6 +915,11 @@
   res.toSet
 }
 
+def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] = {
+  val res = turnIntoTerms((L(r, ctx))).map(oneSimp)
+  res.toSet
+}
+
 def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = {
   subseteqPred(f(a, b), c)
 }
@@ -923,7 +928,9 @@
   res
 }
 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
-  if (ABIncludedByC(r, ctx, acc, attachCtx, rs1_subseteq_rs2)) {//acc.flatMap(breakIntoTerms
+  if (ABIncludedByC(a = r, b = ctx, c = acc, 
+                    f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
+  {//acc.flatMap(breakIntoTerms
     AZERO
   }
   else{
@@ -951,6 +958,36 @@
   }
 }
 
+def prune6cc(acc: Set[Rexp], r: Rexp, ctx: List[Rexp]) : Rexp = {
+  if (ABIncludedByC(a = r, b = ctx, c = acc, 
+                    f = attachCtxcc, subseteqPred = rs1_subseteq_rs2)) 
+  {//acc.flatMap(breakIntoTerms
+    ZERO
+  }
+  else{
+    r match {
+      case SEQ(r1, r2) => 
+      (prune6cc(acc, r1, r2 :: ctx)) match{
+        case ZERO => 
+          ZERO
+        case ONE => 
+          r2
+        case r1p => 
+          SEQ(r1p, r2)
+      }
+      case ALTS(r1, r2) => 
+        List(r1, r2).map(r => prune6cc(acc, r, ctx)).filter(_ != AZERO) match {
+          case Nil => 
+            ZERO
+          case r :: Nil => 
+            r 
+          case ra :: rb :: Nil => 
+            ALTS(ra, rb)
+        }
+      case r => r
+    }
+  }
+}
 
 def distinctBy6(xs: List[ARexp], acc: Set[Rexp] = Set()) : List[ARexp] = xs match {
   case Nil => 
@@ -973,6 +1010,26 @@
   }
 }
 
+def distinctByacc(xs: List[Rexp], acc: Set[Rexp] = Set()) : Set[Rexp] = xs match {
+  case Nil => 
+    acc
+  case x :: xs => {
+    if(acc.contains(x)){
+      distinctByacc(xs, acc)
+    }
+    else{
+      val pruned = prune6cc(acc, x, Nil)
+      val newTerms = turnIntoTerms(pruned)
+      pruned match {
+        case ZERO => 
+          distinctByacc(xs, acc)
+        case xPrime => 
+          distinctByacc(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))
   case ALTS(r1, r2) => breakIntoTerms(r1) ::: breakIntoTerms(r2)
@@ -1380,21 +1437,23 @@
   // }
   
 }
-naive_matcher()
+// naive_matcher()
 def generator_test() {
 
-  test(rexp(4), 1000000) { (r: Rexp) => 
+  test(single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
+  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))), 1) { (r: Rexp) => 
   // ALTS(SEQ(SEQ(ONE,CHAR('a')),STAR(CHAR('a'))),SEQ(ALTS(CHAR('c'),ONE),STAR(ZERO))))))), 1) { (r: Rexp) => 
-    val ss = Set("b")//stringsFromRexp(r)
-    val boolList = ss.filter(s => s != "").map(s => {
+    val ss = stringsFromRexp(r)
+    val boolList = ss.map(s => {
       //val bdStrong = bdersStrong(s.toList, internalise(r))
-      val bdStrong6 = bdersStrong7(s.toList, internalise(r))
+      val bdStrong6 = bdersStrong6(s.toList, internalise(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
+      rs1_subseteq_rs2(bdStrong6Set.toSet, distinctByacc(pdersSet.toList))
+      //bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size ||
+      //rs1_subseteq_rs2(bdStrong6Set.toSet, pdersSet union pdersSetBroken)//|| bdStrong6Set.size <= pdersSetBroken.size
     })
-    //println(boolList)
     //!boolList.exists(b => b == false)
     !boolList.exists(b => b == false)
   }
@@ -1408,13 +1467,19 @@
           //  CHAR('c')))))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE)))
 //counterexample1: STAR(SEQ(ALTS(STAR(ZERO),ALTS(CHAR(a),CHAR(b))),SEQ(ONE,ALTS(CHAR(a),CHAR(b)))))
 //counterexample2: SEQ(ALTS(SEQ(CHAR(a),STAR(ONE)),STAR(ONE)),ALTS(CHAR(a),SEQ(ALTS(CHAR(c),CHAR(a)),CHAR(b))))
+
+//new ce1 : STAR(SEQ(ALTS(ALTS(ONE,CHAR(a)),SEQ(ONE,CHAR(b))),ALTS(CHAR(a),ALTS(CHAR(b),CHAR(a)))))
+//new ce2 : ALTS(CHAR(b),SEQ(ALTS(ZERO,ALTS(CHAR(b),CHAR(b))),ALTS(ALTS(CHAR(a),CHAR(b)),SEQ(CHAR(c),ONE))))
+//new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
 def counterexample_check() {
-  val r = SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
-    ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
+  val r = SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
+  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
+    //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
   val s = "b"
   val bdStrong5 = bdersStrong7(s.toList, internalise(r))
-  val bdStrong5Set = breakIntoTerms(erase(bdStrong5))
+  val bdStrong5Set = turnIntoTerms(erase(bdStrong5))
   val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => turnIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+  val apdersSet = pdersSet.map(internalise)
   println("original regex ")
   rprint(r)
   println("after strong bsimp")
@@ -1423,9 +1488,23 @@
   rsprint(bdStrong5Set)
   println("after pderUNIV")
   rsprint(pdersSet.toList)
+  println("pderUNIV distinctBy6")
+  //asprint(distinctBy6(apdersSet.toList))
+  rsprint(distinctByacc(pdersSet.toList))
+  // rsprint(turnIntoTerms(pdersSet.toList(3)))
+  // println("NO 3 not into terms")
+  // rprint((pdersSet.toList()))
+  // println("after pderUNIV broken")
+  // rsprint(pdersSet.flatMap(r => turnIntoTerms(r)).toList)
 
 }
-// counterexample_check()
+counterexample_check()
+
+def breakable(r: Rexp) : Boolean = r match {
+  case SEQ(ALTS(_, _), _) => true
+  case SEQ(r1, r2) => breakable(r1)
+  case _ => false
+}
 
 def linform_test() {
   val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) //