diff -r 96e93df60954 -r 823d9b19d21c thys2/blexer2.sc
--- a/thys2/blexer2.sc	Mon May 30 17:24:52 2022 +0100
+++ b/thys2/blexer2.sc	Mon May 30 20:36:15 2022 +0100
@@ -521,6 +521,7 @@
         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) => ASEQ(bs1, r1s, r2s)
     }
     case AALTS(bs1, rs) => {
@@ -732,9 +733,9 @@
   res.toSet
 }
 
-def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, inclusionPred: (C, C) => Boolean) : Boolean = {
+def ABIncludedByC[A, B, C](a: A, b: B, c: C, f: (A, B) => C, subseteqPred: (C, C) => Boolean) : Boolean = {
   
-  inclusionPred(f(a, b), c)
+  subseteqPred(f(a, b), c)
 }
 def rexpListInclusion(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = {
   // println("r+ctx---------")
@@ -747,7 +748,7 @@
   // println("end------------------")
   res
 }
-def pAKC6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
+def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
   // println("pakc--------r")
   // println(shortRexpOutput(erase(r)))
   //   println("ctx---------")
@@ -766,7 +767,7 @@
   else{
     r match {
       case ASEQ(bs, r1, r2) => 
-      (pAKC6(acc, r1, erase(r2) :: ctx)) match{
+      (prune6(acc, r1, erase(r2) :: ctx)) match{
         case AZERO => 
           AZERO
         case AONE(bs1) => 
@@ -782,7 +783,7 @@
         // rs0.foreach(r => println(shortRexpOutput(erase(r))))
         // println(s"acc is ")
         // acc.foreach(r => println(shortRexpOutput(r)))
-        rs0.map(r => pAKC6(acc, r, ctx)).filter(_ != AZERO) match {
+        rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
           case Nil => 
             // println("after pruning Nil")
             AZERO
@@ -809,7 +810,7 @@
       distinctBy6(xs, acc)
     }
     else{
-      val pruned = pAKC6(acc, x, Nil)
+      val pruned = prune6(acc, x, Nil)
       val newTerms = strongBreakIntoTerms(erase(pruned))
       pruned match {
         case AZERO => 
@@ -1236,7 +1237,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), 100000) { (r: Rexp) => 
+  test(rexp(8), 10000) { (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.filter(s => s != "").map(s => {
@@ -1256,7 +1257,7 @@
 
 }
 // small()
-// generator_test()
+generator_test()
 
 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)))
@@ -1275,11 +1276,13 @@
 }
 // counterexample_check()
 def linform_test() {
-  val r = STAR(SEQ(STAR(CHAR('c')), ONE))
+  val r = STAR(SEQ(STAR(CHAR('c')),ONE))//SEQ(STAR(CHAR('c')),STAR(SEQ(STAR(CHAR('c')),ONE))) //
   val r_linforms = lf(r)
   println(r_linforms.size)
+  val pderuniv = pderUNIV(r)
+  println(pderuniv.size)
 }
-linform_test()
+// linform_test()
 // 1
 def newStrong_test() {
   val r2 = (CHAR('b') | ONE)