diff -r c334f0b3ef52 -r cc54ce075db5 thys2/blexer2.sc
--- a/thys2/blexer2.sc	Tue May 31 17:36:45 2022 +0100
+++ b/thys2/blexer2.sc	Fri Jun 03 16:45:30 2022 +0100
@@ -522,6 +522,7 @@
         case (_, AZERO) => AZERO
         case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
         case (r1s, AONE(bs2)) => fuse(bs1, r1s) //asserted bs2 == Nil
+        //case (r1s, r2s) if(isOne(erase(r1s))) => fuse(bs1 ++ mkepsBC(r1s), r2s)
         case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
     }
     case AALTS(bs1, rs) => {
@@ -535,10 +536,78 @@
             case rs => AALTS(bs1, rs)  
           }
     }
+    case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
     case r => r
   }
 }
 
+def distinctWith(rs: List[ARexp], 
+                f: (ARexp, Set[Rexp]) => ARexp, 
+                acc: Set[Rexp] = Set()) : List[ARexp] = 
+  rs match{
+    case Nil => Nil
+    case r :: rs => 
+      if(acc(erase(r)))
+        distinctWith(rs, f, acc)
+      else {
+        val pruned_r = f(r, acc)
+        pruned_r :: distinctWith(rs, f, strongBreakIntoTerms(erase(pruned_r)) ++: acc)
+      }
+  }
+
+//r = r' ~ tail => returns r'
+def removeSeqTail(r: Rexp, tail: Rexp) : Rexp = r match {
+  case SEQ(r1, r2) => 
+    if(r2 == tail) 
+      r1
+    else
+      ZERO
+  case r => ZERO
+}
+
+def prune7(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
+  case AALTS(bs, rs) => rs.map(r => prune7(r, acc)).filter(_ != ZERO) match
+  {
+    case Nil => AZERO
+    case r::Nil => fuse(bs, r)
+    case rs1 => AALTS(bs, rs1)
+  }
+  case ASEQ(bs, r1, r2) => prune7(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {
+    case AZERO => AZERO
+    case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)
+    case r1p => ASEQ(bs, r1p, r2)
+  }
+  case r => if(acc(erase(r))) AZERO else r
+}
+
+def strongBsimp7(r: ARexp): ARexp =
+{
+  r match {
+    case ASEQ(bs1, r1, r2) => (strongBsimp7(r1), strongBsimp7(r2)) match {
+        case (AZERO, _) => AZERO
+        case (_, AZERO) => AZERO
+        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
+        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //asserted bs2 == Nil
+        //case (r1s, r2s) if(isOne(erase(r1s))) => fuse(bs1 ++ mkepsBC(r1s), r2s)
+        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
+    }
+    case AALTS(bs1, rs) => {
+        // println("alts case")
+          val rs_simp = rs.map(strongBsimp7(_))
+          val flat_res = flats(rs_simp)
+          var dist_res = distinctWith(flat_res, prune7)//distinctBy(flat_res, erase)
+          (dist_res) match {
+            case Nil => AZERO
+            case s :: Nil => fuse(bs1, s)
+            case rs => AALTS(bs1, rs)  
+          }
+    }
+    case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
+    case r => r
+  }
+}
+
+
 def bders (s: List[Char], r: ARexp) : ARexp = s match {
   case Nil => r
   case c::s => bders(s, bder(c, r))
@@ -717,9 +786,28 @@
   }
 }
 
+def atMostEmpty(r: Rexp) : Boolean = r match {
+  case ZERO => true
+  case ONE => true
+  case STAR(r) => atMostEmpty(r)
+  case SEQ(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
+  case ALTS(r1, r2) => atMostEmpty(r1) && atMostEmpty(r2)
+  case CHAR(_) => false
+}
+
+def isOne(r: Rexp) : Boolean = r match {
+  case ONE => true
+  case SEQ(r1, r2) => isOne(r1) && isOne(r2)
+  case ALTS(r1, r2) => (isOne(r1) || isOne(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
+  case STAR(r0) => atMostEmpty(r0)
+  case CHAR(c) => false
+  case ZERO => false
+
+}
+
 def strongBreakIntoTerms(r: Rexp): List[Rexp] = r match {
-  case SEQ(r1, r2)  => if(nullable(r1)) 
-                          strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2)) ::: 
+  case SEQ(r1, r2)  => if(isOne(r1)) 
+                          //strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2)) ::: 
                           strongBreakIntoTerms(r2) 
                        else 
                           strongBreakIntoTerms(r1).map(r11 => SEQ(r11, r2))
@@ -734,34 +822,14 @@
 }
 
 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)
 }
-def rexpListInclusion(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = {
-  // println("r+ctx---------")
-  // rsprint(rs1)
-  // println("acc---------")
-  // rsprint(rs2)
-  
+def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = {
   val res = rs1.forall(rs2.contains)
-  // println(res)
-  // println("end------------------")
   res
 }
 def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
-  // println("pakc--------r")
-  // println(shortRexpOutput(erase(r)))
-  //   println("ctx---------")
-  // rsprint(ctx)
-  // println("pakc-------acc")
-  // rsprint(acc)
-  // println("r+ctx broken down---------")
-  // 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!!!")
+  if (ABIncludedByC(r, ctx, acc, attachCtx, rs1_subseteq_rs2)) {//acc.flatMap(breakIntoTerms
     AZERO
   }
   else{
@@ -776,23 +844,12 @@
           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 => prune6(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
@@ -913,7 +970,6 @@
 def strong_blex_simp5(r: ARexp, s: List[Char]) : Bits = s match {
   case Nil => {
     if (bnullable(r)) {
-      //println(asize(r))
       val bits = mkepsBC(r)
       bits
     }
@@ -943,6 +999,10 @@
     case Nil => r
     case c::s => bdersStrong6(s, strongBsimp6(bder(c, r)))
   }
+  def bdersStrong7(s: List[Char], r: ARexp) : ARexp = s match {
+    case Nil => r
+    case c::s => bdersStrong7(s, strongBsimp7(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 {
@@ -1189,82 +1249,38 @@
 
 def generator_test() {
 
-  // test(rexp(7), 1000) { (r: Rexp) => 
-  //   val ss = stringsFromRexp(r)
-  //   val boolList = ss.map(s => {
-  //     val simpVal = simpBlexer(r, s)
-  //     val strongVal = strongBlexer(r, s)
-  //     // println(simpVal)
-  //     // println(strongVal)
-  //     (simpVal == strongVal) && (simpVal != None) 
-  //   })
-  //   !boolList.exists(b => b == false)
-  // }
-  // test(single(STAR(ALTS(STAR(CHAR('c')),ALTS(CHAR('c'),ZERO)))), 100000) { (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))
-  //     // println(shortRexpOutput(r))
-  //     // println(s)
-  //     // println(strongVal)
-  //     // println(strongVal5)
-  //     // (strongVal == strongVal5) 
-
-  //     if(asize(bdStrong5) > asize(bdStrong)){
-  //       println(s)
-  //       println(shortRexpOutput(erase(bdStrong5)))
-  //       println(shortRexpOutput(erase(bdStrong)))
-  //     }
-  //     asize(bdStrong5) <= asize(bdStrong)
-  //   })
-  //   !boolList.exists(b => b == false)
-  // }
-  //*** 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(8), 10000) { (r: Rexp) => 
+  test(rexp(4), 1000000) { (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 ss = Set("b")//stringsFromRexp(r)
     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(bdStrong6Set.size, pdersSet.size)
-      bdStrong6Set.size <= pdersSet.size
+      val bdStrong6 = bdersStrong7(s.toList, internalise(r))
+      val bdStrong6Set = strongBreakIntoTerms(erase(bdStrong6))
+      val pdersSet = pderUNIV(r)//.flatMap(r => strongBreakIntoTerms(r))
+      val pdersSetBroken = pdersSet.flatMap(r => strongBreakIntoTerms(r))
+      bdStrong6Set.size <= pdersSet.size || bdStrong6Set.size <= pdersSetBroken.size
     })
-    // println(boolList)
+    //println(boolList)
     //!boolList.exists(b => b == false)
     !boolList.exists(b => b == false)
   }
-
-
 }
 // small()
-generator_test()
-
+//  generator_test()
+  
+  
+  //STAR(STAR(STAR(SEQ(SEQ(ALTS(STAR(ALTS(ONE,CHAR('c'))),
+          //  CHAR('c')),ALTS(CHAR('a'),ALTS(STAR(CHAR('b')),ALTS(CHAR('a'),ZERO)))),
+          //  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))))
 def counterexample_check() {
-  val r = SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE)))//STAR(SEQ(ALTS(STAR(CHAR('c')),CHAR('c')),SEQ(ALTS(CHAR('c'),ONE),ONE)))
-  val s = "ccc"
-  val bdStrong5 = bdersStrong6(s.toList, internalise(r))
+  val r = 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 pdersSet = pderUNIV(r)//.map(oneSimp).flatMap(r => breakIntoTerms(r))
+  val pdersSet = pderUNIV(r)//.map(r => erase(bsimp(internalise(r))))//.flatMap(r => strongBreakIntoTerms(r))//.map(oneSimp).flatMap(r => breakIntoTerms(r))
   println("original regex ")
   rprint(r)
   println("after strong bsimp")
@@ -1273,8 +1289,10 @@
   rsprint(bdStrong5Set)
   println("after pderUNIV")
   rsprint(pdersSet.toList)
+
 }
-// counterexample_check()
+counterexample_check()
+
 def linform_test() {
   val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) //
   val r_linforms = lf(r)