diff -r 1481f465e6ea -r c730d018ebfa thys2/blexer2.sc
--- a/thys2/blexer2.sc	Thu Apr 21 14:58:51 2022 +0100
+++ b/thys2/blexer2.sc	Mon Apr 25 17:00:18 2022 +0100
@@ -479,6 +479,35 @@
   }
 }
 
+def strongBsimp5(r: ARexp): ARexp =
+{
+  // println("was this called?")
+  r match {
+    case ASEQ(bs1, r1, r2) => (strongBsimp5(r1), strongBsimp5(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(strongBsimp5(_))
+
+          val flat_res = flats(rs_simp)
+
+          val dist_res = distinctBy5(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))
@@ -552,14 +581,101 @@
         case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
         case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
       }
-      
     }
 }
 
+// fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
+//   where
+// "pAKC_aux rsa r ctx = (if (L (SEQ (erase r) ( ctx) )) ⊆ (L (erase (AALTs [] rsa))) then AZERO else
+//                           case r of (ASEQ bs r1 r2) ⇒ 
+//                             bsimp_ASEQ bs (pAKC_aux rsa r1 (SEQ  (erase r2) ( ctx) )) r2   |
+//                                     (AALTs bs rs) ⇒ 
+//                             bsimp_AALTs bs (flts (map (λr. pAKC_aux rsa r ( ctx) ) rs) )    |
+//                                     r             ⇒ r
+
+// def canonicalSeq(rs: List[Rexp], acc: Rexp) = rs match {
+//   case r::Nil => SEQ(r, acc)
+//   case Nil => acc
+//   case r1::r2::Nil => SEQ(SEQ(r1, r2), acc)
+// }
+
+
+//the "fake" Language interpretation: just concatenates!
+def L(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
+  case Nil => acc
+  case r :: rs1 => 
+    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
+    AZERO
+  }
+  else{
+    r match {
+      case ASEQ(bs, r1, r2) => 
+      (pAKC(rs, 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"rs is ")
+        // rs.foreach(r => println(shortRexpOutput(r)))
+        rs0.map(r => pAKC(rs, 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 distinctBy5(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)){
+      distinctBy5(xs, acc)
+    }
+    else{
+      val pruned = pAKC(acc, x, Nil)
+      val newTerms = breakIntoTerms(erase(pruned))
+      pruned match {
+        case AZERO => 
+          distinctBy5(xs, acc)
+        case xPrime => 
+          xPrime :: distinctBy5(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)
+  case ZERO => Nil
   case _ => r::Nil
 }
 
@@ -583,7 +699,7 @@
   }
   case (STAR(r1), S::bs) => {
     val (v, bs1) = decode_aux(r1, bs)
-    //println(v)
+    //(v)
     val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
     (Stars(v::vs), bs2)
   }
@@ -614,10 +730,19 @@
   decode(r, strong_blex_simp(internalise(r), s.toList))
 }
 
+def strong_blexing_simp5(r: Rexp, s: String) : Val = {
+  decode(r, strong_blex_simp5(internalise(r), s.toList))
+}
+
+
 def strongBlexer(r: Rexp, s: String) : Val = {
   Try(strong_blexing_simp(r, s)).getOrElse(Failure)
 }
 
+def strongBlexer5(r: Rexp, s: String): Val = {
+  Try(strong_blexing_simp5(r, s)).getOrElse(Failure)
+}
+
 def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
   case Nil => {
     if (bnullable(r)) {
@@ -635,15 +760,36 @@
   }
 }
 
+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
+    }
+    else 
+      throw new Exception("Not matched")
+  }
+  case c::cs => {
+    val der_res = bder(c,r)
+    val simp_res = strongBsimp5(der_res)  
+    strong_blex_simp5(simp_res, cs)      
+  }
+}
 
 
   def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
     case Nil => r
     case c::s => 
-      println(erase(r))
+      //println(erase(r))
       bders_simp(s, bsimp(bder(c, r)))
   }
   
+  def bdersStrong5(s: List[Char], r: ARexp) : ARexp = s match {
+    case Nil => r
+    case c::s => bdersStrong5(s, strongBsimp5(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 {
@@ -913,58 +1059,54 @@
 }
 
 def generator_test() {
-  // println("XXX generates 10 random integers in the range 0..2") 
-  // println(range(0, 3).gen(10).mkString("\n"))
-
-  // println("XXX gnerates random lists and trees")
-  // println(lists.generate())
-  // println(trees(chars).generate())
-
-  // println("XXX generates 10 random characters") 
-  // println(chars.gen(10).mkString("\n"))  
 
-  // println("XXX generates 10 random leaf-regexes") 
-  // println(leaf_rexp().gen(10).mkString("\n"))
-  
-  // println("XXX generates 1000 regexes of maximal 10 height")
-  // println(rexp(10).gen(1000).mkString("\n"))
-  
-  // println("XXX generates 1000 regexes and tests an always true-test")
-  // test(rexp(10), 1000) { _ => true }
-  // println("XXX generates regexes and tests a valid predicate")  
-  // test(rexp(10), 1000) { r => height(r) <= size(r) }
-  // println("XXX faulty test")
-  // test(rexp(10), 100) { r => height(r) <= size_faulty(r) }
-
+  // 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) 
 
-  /* For inspection of counterexamples should they arise*/
-//   println("testing strongbsimp against bsimp")
-//   val r = 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'))),
-// SEQ(CHAR('a'),SEQ(ALTS(CHAR('b'),ZERO),SEQ(ONE,CHAR('b'))))),ONE)))),ONE))
-
-//     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) 
-//     })
-//     println(boolList)
-//     println(boolList.exists(b => b == false))
-
-
-  test(rexp(9), 100000) { (r: Rexp) => 
+  //     if(asize(bdStrong5) > asize(bdStrong)){
+  //       println(s)
+  //       println(shortRexpOutput(erase(bdStrong5)))
+  //       println(shortRexpOutput(erase(bdStrong)))
+  //     }
+  //     asize(bdStrong5) <= asize(bdStrong)
+  //   })
+  //   !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) =>
     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) 
+      val bdStrong = bdersStrong(s.toList, internalise(r))
+      val bdStrong5 = bdersStrong5(s.toList, internalise(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(boolList)
     !boolList.exists(b => b == false)
   }