--- a/thys2/blexer2.sc	Tue Nov 22 12:50:04 2022 +0000
+++ b/thys2/blexer2.sc	Sat Nov 26 16:18:10 2022 +0000
@@ -661,17 +661,22 @@
       }
 
     //r = r' ~ tail' : If tail' matches 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 removeSeqTail(r: Rexp, tail: Rexp) : Rexp = 
+      if (r == tail)
+        ONE
+      else {
+        r match {
+          case SEQ(r1, r2) => 
+            if(r2 == tail) 
+              r1
+            else
+              ZERO
+          case r => ZERO
+        }
+      }
 
     def prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
-      case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != ZERO) match
+      case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != AZERO) match
       {
         //all components have been removed, meaning this is effectively a duplicate
         //flats will take care of removing this AZERO 
@@ -911,13 +916,14 @@
     }
 
     def turnIntoTerms(r: Rexp): List[Rexp] = r match {
-      case SEQ(r1, r2)  => if(isOne1(r1)) 
-      turnIntoTerms(r2) 
-    else 
-      turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
-      case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
-      case ZERO => Nil
-      case _ => r :: Nil
+      case SEQ(r1, r2)  => 
+    //   if(isOne1(r1)) 
+    //   turnIntoTerms(r2) 
+    // else 
+        turnIntoTerms(r1).flatMap(r11 => furtherSEQ(r11, r2))
+          case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
+          case ZERO => Nil
+          case _ => r :: Nil
     }
 
     def furtherSEQ(r11: Rexp, r2: Rexp) : List[Rexp] = {
@@ -1544,25 +1550,29 @@
     //new ce3 : SEQ(CHAR(b),ALTS(ALTS(ALTS(ONE,CHAR(a)),SEQ(CHAR(c),ONE)),SEQ(STAR(ZERO),SEQ(ONE,CHAR(b)))))
     //circular double-nullable STAR(SEQ((STAR("b") | "a" | "b"), ("b" | ONE)))
     def counterexample_check() {
-      val r = STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
-        ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
+      val r : Rexp = SEQ(ALTS(ONE, 
+        SEQ(ALTS(CHAR('f'), CHAR('b')), CHAR('g'))), SEQ(CHAR('a'), SEQ(CHAR('d'), CHAR('e'))))//(1+(f +b)·g)·(a·(d·e))//STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),
+      val acc : Set[Rexp] = Set(SEQ(CHAR('a'), SEQ(CHAR('d'), CHAR('e'))), SEQ(SEQ(CHAR('f'), CHAR('g')), SEQ(CHAR('a'), SEQ(CHAR('d'), CHAR('e')))) )
+      val a = internalise(r)
+      aprint(prune(a, acc));
+        //ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))//SEQ(SEQ(STAR(ALTS(CHAR('a'),CHAR('b'))),
       //ALTS(ALTS(CHAR('c'),CHAR('b')),STAR(ONE))),STAR(CHAR('b')))
-      val s = "ab"
-      val bdStrong5 = bdersStrong6(s.toList, internalise(r))
-      val bdStrong5Set = breakIntoTerms(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")
-      aprint(bdStrong5)
-      println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   ")
-      rsprint(bdStrong5Set)
-      println("after pderUNIV")
-      rsprint(pdersSet.toList)
-      println("pderUNIV distinctBy6")
-      //asprint(distinctBy6(apdersSet.toList))
-      rsprint((pdersSet.toList).flatMap(turnIntoTerms))
+      // val s = "ab"
+      // val bdStrong5 = bdersStrong6(s.toList, internalise(r))
+      // val bdStrong5Set = breakIntoTerms(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")
+      // aprint(bdStrong5)
+      // println("turned into a set %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%   ")
+      // rsprint(bdStrong5Set)
+      // println("after pderUNIV")
+      // rsprint(pdersSet.toList)
+      // println("pderUNIV distinctBy6")
+      // //asprint(distinctBy6(apdersSet.toList))
+      // rsprint((pdersSet.toList).flatMap(turnIntoTerms))
       // rsprint(turnIntoTerms(pdersSet.toList(3)))
       // println("NO 3 not into terms")
       // rprint((pdersSet.toList()))
@@ -1586,7 +1596,7 @@
 
     }
 
-    lf_display()
+    // lf_display()
 
     def breakable(r: Rexp) : Boolean = r match {
       case SEQ(ALTS(_, _), _) => true
@@ -1657,3 +1667,5 @@
 
 
 
+println("hi!!!!!")
+counterexample_check()
\ No newline at end of file