--- a/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Wed Aug 31 23:57:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Bitcoded2.tex	Thu Sep 01 23:47:37 2022 +0100
@@ -557,7 +557,7 @@
 
 	\inferrule * [Right = $LS$] {\vspace{0em}}{_{bs} \sum (rs_1 :: rs_b) \stackrel{s}{\rightsquigarrow} ((\map \; (\fuse \; bs_1) \; rs_1) @ rsb) }
 
-	\inferrule * [Right = $LD$] {\\ \rerase{a_1} = \rerase{a_2}}{rs_a @ [a_1] @ rs_b @ [a_2] @ rsc \stackrel{s}{\rightsquigarrow} rs_a @ [a_1] @ rs_b @ rs_c}
+	\inferrule * [Right = $LD$] {\\ \rerase{a_1} = \rerase{a_2}}{rs_a @ [a_1] @ rs_b @ [a_2] @ rs_c \stackrel{s}{\rightsquigarrow} rs_a @ [a_1] @ rs_b @ rs_c}
 
 \end{mathpar}
 \caption{

--- a/ChengsongTanPhdThesis/Chapters/Cubic.tex	Wed Aug 31 23:57:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Cubic.tex	Thu Sep 01 23:47:37 2022 +0100
@@ -59,239 +59,152 @@
 \section{A Stronger Version of Simplification}
 %TODO: search for isabelle proofs of algorithms that check equivalence 
 In our bitcoded lexing algorithm, (sub)terms represent (sub)matches.
-For example, the regular expression $aa \cdot a^*+ a \cdot a^*$ contains two terms, 
-which expresses two possibilities it will match future input.
-It will either match 2 $a$'s, then 0 or more $a$'s, in other words, at least 2 more $a$'s
-\begin{figure}\label{string_3parts1}
+For example, the regular expression 
+\[
+	aa \cdot a^*+ a \cdot a^* + aa\cdot a^*
+\]
+contains three terms, 
+expressing three possibilities it will match future input.
+The first and the third terms are identical, which means we can eliminate
+the latter as we know it will not be picked up by $\bmkeps$.
+In $\bsimps$, the $\distinctBy$ function takes care of this.
+The criteria $\distinctBy$ uses for removing a duplicate
+$a_2$ in the list
+\begin{center}
+	$rs_a@[a_1]@rs_b@[a_2]@rs_c$
+\end{center}
+is that 
 \begin{center}
-\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
-    \node [rectangle split, rectangle split horizontal, rectangle split parts=3]
-        {Consumed Input
-        \nodepart{two} Expects $aa$
-         \nodepart{three} Then expects $a^*$};
-
+	$\rerase{a_1} = \rerase{a_2}$.
+\end{center}
+It can be characterised as the $LD$ 
+rewrite rule in \ref{rrewriteRules}.\\
+The problem , however, is that identical components
+in two slightly different regular expressions cannot be removed:
+\begin{figure}[H]
+\[
+	(a+b+d) \cdot r_1 + (a+c+e) \cdot r_1 \stackrel{?}{\rightsquigarrow} (a+b+d) \cdot r_1 + (c+e) \cdot r_1
+\]
+\caption{Desired simplification, but not done in $\blexersimp$}\label{partialDedup}
+\end{figure}
+\noindent
+A simplification like this actually
+cannot be omitted,
+as without it the size could blow up even with our $\simp$ function:
+\begin{figure}[H]
+\centering
+\begin{tikzpicture}
+\begin{axis}[
+    %xlabel={$n$},
+    myplotstyle,
+    xlabel={input length},
+    ylabel={size},
+    ]
+\addplot[blue,mark=*, mark options={fill=white}] table {bsimpExponential.data};
+\end{axis}
 \end{tikzpicture}
-\end{center}
+\caption{Runtime of $\blexersimp$ for matching 
+	$\protect((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ 
+	with strings 
+	of the form $\protect\underbrace{aa..a}_{n}$.}\label{blexerExp}
+\end{figure}
+\noindent
+We would like to apply the rewriting at some stage
+\begin{figure}[H]
+\[
+	(a+b+d) \cdot r_1  \longrightarrow a \cdot r_1 + b \cdot r_1 + d \cdot r_1
+\]
+\caption{Desired simplification, but not done in $\blexersimp$}\label{desiredSimp}
 \end{figure}
 \noindent
-Or it will match at least 1 more $a$:
-\begin{figure}\label{string_3parts2}
-\begin{center}
-\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
-    \node [rectangle split, rectangle split horizontal, rectangle split parts=3]
-        {Consumed
-        \nodepart{two} Expects $a$
-         \nodepart{three} Then expects $a^*$};
-
-\end{tikzpicture}
-\end{center}
-\end{figure}
-If these two possibilities are identical, we can eliminate
-the second one as we know the second one corresponds to 
-a match that is not $\POSIX$.
-
-
-If two identical regexes 
-happen to be grouped into different sequences, one cannot use
-the $a + a \rightsquigarrow a$ rule to eliminate them, even if they 
-are "parallel" to each other:
-\[
-(a+b) \cdot r_1 + (a+c) \cdot r_2 \rightsquigarrow (a+b) \cdot r_1 + (c) \cdot r_2
-\]
-and that's because they are followed by possibly 
-different "suffixes" $r_1$ and $r_2$, and if 
-they do turn out to be different then doing 
-\[
-(a+b) \cdot r_1 + (a+c) \cdot r_2 \rightsquigarrow (a+b) \cdot r_1 + (c) \cdot r_2
-\]
-might cause a possible match where the string is in $L(a \cdot r_2)$ to be lost.
-
-Here is an example for this.
-Assume we have the derivative regex 
-\[( r_1  +  r_2  +  r_3)\cdot r+ 
-( r_1  +  r_5  +  r_6)\cdot( r_1  +  r_2  +  r_3)^*
-\]
-
-occurring in an intermediate step in our bit-coded lexing algorithm.
+in our $\simp$ function,
+so that it makes the simplification in \ref{partialDedup} possible.
+For example,
+can a function like the below one be used?
+%TODO: simp' that spills things
 
-In this expression, there will be 6 "parallel" terms if we break up regexes 
-of shape $(a+b)\cdot c$ using the distributivity law (into $ac + bc$).
-\begin{align}
-(\nonumber \\
- r_1  + &    \label{term:1} \\
- r_2  + &  \label{term:2} \\
- r_3 &  \label{term:3} \\
-&	)\cdot r\; + \; (\nonumber \\
- r_1  + & \label{term:4} \\
- r_5  + & \label{term:5} \\
- r_6 \label{term:6}\\
-&      )\cdot r\nonumber
-\end{align}
-
-They have been labelled, and each label denotes  
-one term, for example, \ref{term:1} denotes
-\[
- r_1 \cdot r
-\]
-\noindent
-and \ref{term:3} denotes
-\[
- r_3\cdot r.
-\]
-From a lexer's point of view, \ref{term:4} will never 
-be picked up in later phases of matching because there
-is a term \ref{term:1} giving identical matching information.
-The first term \ref{term:1} will match a string in $L(r_1 \cdot  r)$, 
-and so on for term \ref{term:2}, \ref{term:3}, etc.
-
-\mybox{previous input $\ldots$}\mybox{$aaa$ }\mybox{rest of input $\ldots$}
-\begin{center}\label{string_2parts}
-
-\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
-    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]
-        {$r_{x1}$
-         \nodepart{two} $r_1\cdot r$ };
-%\caption{term 1 \ref{term:1}'s matching configuration}
-\end{tikzpicture}
-
+Unfortunately,
+if we introduce them in our
+setting we would lose the POSIX property of our calculated values. 
+For example given the regular expression 
+\begin{center}
+	$(a + ab)(bc + c)$
+\end{center}
+and the string
+\begin{center}
+	$ab$,
 \end{center}
-For term 1 \ref{term:1}, whatever was before the current
-input position was fully matched and the regex corresponding
-to it reduced to $\ONE$, 
-and in the next input token, it will start on $r_1\cdot r$.
-The resulting value will be something of a similar configuration:
-\begin{center}\label{value_2parts}
-%\caption{term 1 \ref{term:1}'s matching configuration}
-\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
-    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]
-        {$v_{x1}$
-         \nodepart{two} $v_{r_1\cdot r}$ };
-\end{tikzpicture}
+then our algorithm generates the following
+correct POSIX value
+\begin{center}
+	$\Seq \; (\Right \; ab) \; (\Right \; c)$.
 \end{center}
-For term 2 \ref{term:2} we have a similar value partition:
-\begin{center}\label{value_2parts2}
-%\caption{term 1 \ref{term:1}'s matching configuration}
-\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
-    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]
-        {$v_{x2}$
-         \nodepart{two} $v_{r_2\cdot r}$ };
-\end{tikzpicture}
+Essentially it matches the string with the longer Right-alternative
+in the first sequence (and
+then the 'rest' with the character regular expression $c$ from the second sequence).
+If we add the simplification above, then we obtain the following value
+\begin{center}
+	$\Left \; (\Seq \; a \; (\Left \; bc))$
+\end{center}
+where the $\Left$-alternatives get priority. 
+However this violates the POSIX rules.
+The reason for getting this undesired value
+is that the new rule splits this regular expression up into 
+\begin{center}
+	$a\cdot(b c + c) + ab \cdot (bc + c)$,
 \end{center}
-\noindent
-and so on.
-We note that for term 4 \ref{term:4} its result value 
-after any position beyond  the current one will always
-be the same:
-\begin{center}\label{value_2parts4}
-%\caption{term 1 \ref{term:1}'s matching configuration}
-\begin{tikzpicture}[every node/.append style={draw, rounded corners, inner sep=10pt}]
-    \node [rectangle split, rectangle split horizontal, rectangle split parts=2]
-        {$v_{x4}$
-         \nodepart{two} $v_{r_1\cdot r}$ };
-\end{tikzpicture}
+which becomes a regular expression with a 
+totally different structure--the original
+was a sequence, and now it becomes an alternative.
+With an alternative the maximum munch rule no longer works.\\
+A method to reconcile this is to do the 
+transformation in \ref{desiredSimp} ``non-invasively'',
+meaning that we traverse the list of regular expressions
+\begin{center}
+	$rs_a@[a]@rs_c$
+\end{center}
+in the alternative
+\begin{center}
+	$\sum ( rs_a@[a]@rs_c)$
 \end{center}
-And $\POSIX$ rules says that we can eliminate at least one of them.
-Our algorithm always puts the regex with the longest initial sub-match at the left of the 
-alternatives, so we safely throw away \ref{term:4}.
-The fact that term 1 and 4 are not immediately in the same alternative
-expression does not prevent them from being two duplicate matches at
-the current point of view.
-To implement this idea into an algorithm, we define a "pruning function"
-$\textit{prune}$, that takes away parts of all terms in $r$ that belongs to
-$\textit{acc}$, which acts as an element
-is a stronger version of $\textit{distinctBy}$.
-Here is a concise version of it (in the style of Scala):
-\begin{figure}[H]
-\begin{lstlisting}
-def distinctByPlus(rs: List[ARexp], acc: Set[Rexp] = Set()) : 
-List[ARexp] =  rs match {
-  case Nil => Nil
-  case r :: rs =>
-    if(acc.contains(erase(r)))
-      distinctByPlus(rs, acc)
-    else 
-      prune(r, acc) :: distinctByPlus(rs, prune(r, acc) +: acc)
-}
-
-\end{lstlisting}
-\caption{the distinctByPlus function}
-\end{figure}
-But for the function $\textit{prune}$ there is a difficulty:
-how could one define the $L$ function in a "computable" way,
-so that they generate a (lazy infinite) set of strings in $L(r)$.
-We also need a function that tests whether $L(r_1) \subseteq L(r_2)$
-is true.
-For the moment we cut corners and do not define these two functions
-as they are not used by Antimirov (and will probably not contribute
-to a bound better than Antimirov's cubic bound).
-Rather, we do not try to eliminate in every instance of regular expressions
-that have "language duplicates", but only eliminate the "exact duplicates".
-For this we need to break up terms $(a+b)\cdot c$ into two
-terms $a\cdot c$ and $b\cdot c$ before we add them to the accumulator:
+using  a function similar to $\distinctBy$,
+but this time 
+we allow a more general list rewrite:
+	\begin{mathpar}
+		\inferrule{\vspace{0mm} }{rs_a@[a]@rs_c 
+			\stackrel{s}{\rightsquigarrow }
+		rs_a@[\textit{prune} \; a \; rs_a]@rs_c }
+	\end{mathpar}
+%L \; a_1' = L \; a_1 \setminus (\cup_{a \in rs_a} L \; a)
+where $\textit{prune} \;a \; acc$ traverses $a$
+without altering the structure of $a$, removing components in $a$
+that have appeared in the accumulator $acc$.
+For example
+\begin{center}
+	$\textit{prune} \;\;\; (r_a+r_f+r_g+r_h)r_d \;\; \; [(r_a+r_b+r_c)r_d, (r_e+r_f)r_d] $
+\end{center}
+should be equal to 
+\begin{center}
+	$(r_g+r_h)r_d$
+\end{center}
+because $r_gr_d$ and 
+$r_hr_d$ are the only terms
+that have not appeared in the accumulator list 
+\begin{center}
+$[(r_a+r_b+r_c)r_d, (r_e+r_f)r_d]$.
+\end{center}
+We implemented 
+function $\textit{prune}$ in Scala,
+and incorporated into our lexer,
+by replacing the $\simp$ function 
+with a stronger version called $\bsimpStrong$
+that prunes regular expressions.
+We call this lexer $\blexerStrong$.
+$\blexerStrong$ is able to drastically reduce the
+internal data structure size which could
+trigger exponential behaviours in
+$\blexersimp$.
 \begin{figure}[H]
-\begin{lstlisting}
-def distinctWith(rs: List[ARexp], 
-                pruneFunction: (ARexp, Set[Rexp]) => ARexp, 
-                acc: Set[Rexp] = Set()) : List[ARexp] = 
-  rs match{
-    case Nil => Nil
-    case r :: rs => 
-      if(acc(erase(r)))
-        distinctWith(rs, pruneFunction, acc)
-      else {
-        val pruned_r = pruneFunction(r, acc)
-        pruned_r :: 
-        distinctWith(rs, 
-          pruneFunction, 
-          turnIntoTerms(erase(pruned_r)) ++: acc
-        )
-      }
-  }
-\end{lstlisting}
-\caption{A Stronger Version of $\textit{distinctBy}$}
-\end{figure}
-\noindent
-This process is done by the function $\textit{turnIntoTerms}$:
-\begin{figure}
-\begin{verbatim}
-def turnIntoTerms(r: Rexp): List[Rexp] = r match {
-  case SEQ(r1, r2)  => if(isOne(r1)) 
-                          turnIntoTerms(r2) 
-                       else 
-                          turnIntoTerms(r1).map(r11 => SEQ(r11, r2))
-  case ALTS(r1, r2) => turnIntoTerms(r1) ::: turnIntoTerms(r2)
-  case ZERO => Nil
-  case _ => r :: Nil
-}
-\end{verbatim}
-\caption{function that breaks up regular expression into "atomic" terms}
-\end{figure}
-
-\noindent
-The pruning function can be defined recursively:
-\begin{figure}
-\begin{verbatim}
-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
-}
-\end{verbatim}
-\caption{pruning function}
-\end{figure}
-
-
-
-\begin{figure}
 \centering
 \begin{tabular}{@{}c@{\hspace{0mm}}c@{\hspace{0mm}}c@{}}
 \begin{tikzpicture}
@@ -316,10 +229,275 @@
 \end{axis}
 \end{tikzpicture}\\
 \multicolumn{2}{l}{Graphs: Runtime for matching $((a^* + (aa)^* + \ldots + (aaaaa)^* )^*)^*$ with strings 
-           of the form $\underbrace{aa..a}_{n}$.}
+	   of the form $\underbrace{aa..a}_{n}$.}
 \end{tabular}    
 \caption{aaaaaStarStar} \label{fig:aaaaaStarStar}
 \end{figure}
+\begin{figure}[H]
+\begin{lstlisting}
+    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
+    }
+
+    //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 prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
+      case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != ZERO) match
+      {
+        //all components have been removed, meaning this is effectively a duplicate
+        //flats will take care of removing this AZERO 
+        case Nil => AZERO
+        case r::Nil => fuse(bs, r)
+        case rs1 => AALTS(bs, rs1)
+      }
+      case ASEQ(bs, r1, r2) => 
+        //remove the r2 in (ra + rb)r2 to identify the duplicate contents of r1
+        prune(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {
+          //after pruning, returns 0
+          case AZERO => AZERO
+          //after pruning, got r1'.r2, where r1' is equal to 1
+          case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)
+          //assemble the pruned head r1p with r2
+          case r1p => ASEQ(bs, r1p, r2)
+        }
+        //this does the duplicate component removal task
+      case r => if(acc(erase(r))) AZERO else r
+    }
+\end{lstlisting}
+\caption{pruning function together with its helper functions}
+\end{figure}
+\noindent
+The benefits of using 
+$\textit{prune}$ such as refining the finiteness bound
+to a cubic bound has not been formalised yet.
+Therefore we choose to use Scala code rather than an Isabelle-style formal 
+definition like we did for $\simp$, as the definitions might change
+to suit proof needs.
+In the rest of the chapter we will use this convention consistently.
+\begin{figure}[H]
+\begin{lstlisting}
+  def distinctWith(rs: List[ARexp], 
+    pruneFunction: (ARexp, Set[Rexp]) => ARexp, 
+    acc: Set[Rexp] = Set()) : List[ARexp] = 
+      rs match{
+        case Nil => Nil
+        case r :: rs => 
+          if(acc(erase(r)))
+            distinctWith(rs, pruneFunction, acc)
+          else {
+            val pruned_r = pruneFunction(r, acc)
+            pruned_r :: 
+            distinctWith(rs, 
+              pruneFunction, 
+              turnIntoTerms(erase(pruned_r)) ++: acc
+              )
+          }
+      }
+\end{lstlisting}
+\caption{A Stronger Version of $\textit{distinctBy}$}
+\end{figure}
+\noindent
+The function $\textit{prune}$ is used in $\distinctWith$.
+$\distinctWith$ is a stronger version of $\distinctBy$
+which not only removes duplicates as $\distinctBy$ would
+do, but also uses the $\textit{pruneFunction}$
+argument to prune away verbose components in a regular expression.\\
+\begin{figure}[H]
+\begin{lstlisting}
+   //a stronger version of simp
+    def bsimpStrong(r: ARexp): ARexp =
+    {
+      r match {
+        case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {
+          //normal clauses same as simp
+        case (AZERO, _) => AZERO
+        case (_, AZERO) => AZERO
+        case (AONE(bs2), r2s) => fuse(bs1 ++ bs2, r2s)
+        //bs2 can be discarded
+        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil
+        case (r1s, r2s) => ASEQ(bs1, r1s, r2s)
+        }
+        case AALTS(bs1, rs) => {
+          //distinctBy(flat_res, erase)
+          distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {
+            case Nil => AZERO
+            case s :: Nil => fuse(bs1, s)
+            case rs => AALTS(bs1, rs)
+          }
+        }
+        //stars that can be treated as 1
+        case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
+        case r => r
+      }
+    }
+\end{lstlisting}
+\caption{The function $\bsimpStrong$ and $\bdersStrongs$}
+\end{figure}
+\noindent
+$\distinctWith$, is in turn used in $\bsimpStrong$:
+\begin{figure}[H]
+\begin{lstlisting}
+      //Conjecture: [| bdersStrong(s, r) |] = O([| r |]^3)
+      def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
+        case Nil => r
+        case c::s => bdersStrong(s, bsimpStrong(bder(c, r)))
+      }
+\end{lstlisting}
+\caption{The function $\bsimpStrong$ and $\bdersStrongs$}
+\end{figure}
+\noindent
+We conjecture that the above Scala function $\bdersStrongs$,
+written $\bdersStrong{\_}{\_}$ as an infix notation, 
+satisfies the following property:
+\begin{conjecture}
+	$\llbracket \bdersStrong{a}{s} \rrbracket = O(\llbracket a \rrbracket^3)$
+\end{conjecture}
+The stronger version of $\blexersimp$'s
+code in Scala looks like: 
+\begin{figure}[H]
+\begin{lstlisting}
+      def strongBlexer(r: Rexp, s: String) : Option[Val] = {
+        Try(Some(decode(r, strong_blex_simp(internalise(r), s.toList)))).getOrElse(None)
+      }
+      def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
+        case Nil => {
+          if (bnullable(r)) {
+            mkepsBC(r)
+          }
+          else
+            throw new Exception("Not matched")
+        }
+        case c::cs => {
+          strong_blex_simp(strongBsimp(bder(c, r)), cs)
+        }
+      }
+\end{lstlisting}
+\end{figure}
+\noindent
+We would like to preserve the correctness like the one 
+we had for $\blexersimp$:
+\begin{conjecture}\label{cubicConjecture}
+	$\blexerStrong \;r \; s = \blexer\; r\;s$
+\end{conjecture}
+
+To implement this idea into an algorithm, we define a "pruning function"
+$\textit{prune}$, that takes away parts of all terms in $r$ that belongs to
+$\textit{acc}$, which acts as an element
+is a stronger version of $\textit{distinctBy}$.
+Here is a concise version of it (in the style of Scala):
+
+
+
+
+\noindent
+The pruning function can be defined recursively:
+
+
+
+
+This suggests a link towrads "partial derivatives"
+ introduced by Antimirov \cite{Antimirov95}.
+ 
+ \section{Antimirov's partial derivatives}
+ The idea behind Antimirov's partial derivatives
+is to do derivatives in a similar way as suggested by Brzozowski, 
+but maintain a set of regular expressions instead of a single one:
+
+%TODO: antimirov proposition 3.1, needs completion
+ \begin{center}  
+ \begin{tabular}{ccc}
+ $\partial_x(a+b)$ & $=$ & $\partial_x(a) \cup \partial_x(b)$\\
+$\partial_x(\ONE)$ & $=$ & $\phi$
+\end{tabular}
+\end{center}
+
+Rather than joining the calculated derivatives $\partial_x a$ and $\partial_x b$ together
+using the alternatives constructor, Antimirov cleverly chose to put them into
+a set instead.  This breaks the terms in a derivative regular expression up, 
+allowing us to understand what are the "atomic" components of it.
+For example, To compute what regular expression $x^*(xx + y)^*$'s 
+derivative against $x$ is made of, one can do a partial derivative
+of it and get two singleton sets $\{x^* \cdot (xx + y)^*\}$ and $\{x \cdot (xx + y) ^* \}$
+from $\partial_x(x^*) \cdot (xx + y) ^*$ and $\partial_x((xx + y)^*)$.
+To get all the "atomic" components of a regular expression's possible derivatives,
+there is a procedure Antimirov called $\textit{lf}$, short for "linear forms", that takes
+whatever character is available at the head of the string inside the language of a
+regular expression, and gives back the character and the derivative regular expression
+as a pair (which he called "monomial"):
+ \begin{center}  
+ \begin{tabular}{ccc}
+ $\lf(\ONE)$ & $=$ & $\phi$\\
+$\lf(c)$ & $=$ & $\{(c, \ONE) \}$\\
+ $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
+ $\lf(r^*)$ & $=$ & $\lf(r) \bigodot \lf(r^*)$\\
+\end{tabular}
+\end{center}
+%TODO: completion
+
+There is a slight difference in the last three clauses compared
+with $\partial$: instead of a dot operator $ \textit{rset} \cdot r$ that attaches the regular 
+expression $r$ with every element inside $\textit{rset}$ to create a set of 
+sequence derivatives, it uses the "circle dot" operator $\bigodot$ which operates 
+on a set of monomials (which Antimirov called "linear form") and a regular 
+expression, and returns a linear form:
+ \begin{center}  
+ \begin{tabular}{ccc}
+ $l \bigodot (\ZERO)$ & $=$ & $\phi$\\
+ $l \bigodot (\ONE)$ & $=$ & $l$\\
+ $\phi \bigodot t$ & $=$ & $\phi$\\
+ $\{ (x, \ZERO) \} \bigodot t$ & $=$ & $\{(x,\ZERO) \}$\\
+ $\{ (x, \ONE) \} \bigodot t$ & $=$ & $\{(x,t) \}$\\
+  $\{ (x, p) \} \bigodot t$ & $=$ & $\{(x,p\cdot t) \}$\\
+ $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
+ $\lf(r^*)$ & $=$ & $\lf(r) \cdot \lf(r^*)$\\
+\end{tabular}
+\end{center}
+%TODO: completion
+
+ Some degree of simplification is applied when doing $\bigodot$, for example,
+ $l \bigodot (\ZERO) = \phi$ corresponds to $r \cdot \ZERO \rightsquigarrow \ZERO$,
+ and  $l \bigodot (\ONE) = l$ to $l \cdot \ONE \rightsquigarrow l$, and
+  $\{ (x, \ZERO) \} \bigodot t = \{(x,\ZERO) \}$ to $\ZERO \cdot x \rightsquigarrow \ZERO$,
+  and so on.
+  
+  With the function $\lf$ one can compute all possible partial derivatives $\partial_{UNIV}(r)$ of a regular expression $r$ with 
+  an iterative procedure:
+   \begin{center}  
+ \begin{tabular}{llll}
+$\textit{while}$ & $(\Delta_i \neq \phi)$  &                &          \\
+ 		       &  $\Delta_{i+1}$           &        $ =$ & $\lf(\Delta_i) - \PD_i$ \\
+		       &  $\PD_{i+1}$              &         $ =$ & $\Delta_{i+1} \cup \PD_i$ \\
+$\partial_{UNIV}(r)$ & $=$ & $\PD$ &		     
+\end{tabular}
+\end{center}
+
+
+ $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$,
+
+
 
 
 
@@ -345,22 +523,22 @@
 ~r \backslash c = ~ (r \backslash c)
 \]
  
-The most tricky part of lexing for the $~r$ regex
+The most tricky part of lexing for the $~r$ regular expression
  is creating a value for it.
  For other regular expressions, the value aligns with the 
- structure of the regex:
+ structure of the regular expression:
  \[
  \vdash \Seq(\Char(a), \Char(b)) : a \cdot b
  \]
-But for the $~r$ regex, $s$ is a member of it if and only if
+But for the $~r$ regular expression, $s$ is a member of it if and only if
 $s$ does not belong to $L(r)$. 
 That means when there
-is a match for the not regex, it is not possible to generate how the string $s$ matched
+is a match for the not regular expression, it is not possible to generate how the string $s$ matched
 with $r$. 
 What we can do is preserve the information of how $s$ was not matched by $r$,
 and there are a number of options to do this.
 
-We could give a partial value when there is a partial match for the regex inside
+We could give a partial value when there is a partial match for the regular expression inside
 the $\mathbf{not}$ construct.
 For example, the string $ab$ is not in the language of $(a\cdot b) \cdot c$,
 A value for it could be 

--- a/ChengsongTanPhdThesis/Chapters/Finite.tex	Wed Aug 31 23:57:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Finite.tex	Thu Sep 01 23:47:37 2022 +0100
@@ -2007,108 +2007,10 @@
 \multicolumn{3}{c}{Graphs: size change of 3 randomly generated regular expressions $w.r.t.$ input string length.}
 \end{tabular}    
 \end{center}  
-
-
-
-
-
 \noindent
 Most of the regex's sizes seem to stay within a polynomial bound $w.r.t$ the 
 original size.
-This suggests a link towrads "partial derivatives"
- introduced by Antimirov \cite{Antimirov95}.
- 
- \section{Antimirov's partial derivatives}
- The idea behind Antimirov's partial derivatives
-is to do derivatives in a similar way as suggested by Brzozowski, 
-but maintain a set of regular expressions instead of a single one:
-
-%TODO: antimirov proposition 3.1, needs completion
- \begin{center}  
- \begin{tabular}{ccc}
- $\partial_x(a+b)$ & $=$ & $\partial_x(a) \cup \partial_x(b)$\\
-$\partial_x(\ONE)$ & $=$ & $\phi$
-\end{tabular}
-\end{center}
-
-Rather than joining the calculated derivatives $\partial_x a$ and $\partial_x b$ together
-using the alternatives constructor, Antimirov cleverly chose to put them into
-a set instead.  This breaks the terms in a derivative regular expression up, 
-allowing us to understand what are the "atomic" components of it.
-For example, To compute what regular expression $x^*(xx + y)^*$'s 
-derivative against $x$ is made of, one can do a partial derivative
-of it and get two singleton sets $\{x^* \cdot (xx + y)^*\}$ and $\{x \cdot (xx + y) ^* \}$
-from $\partial_x(x^*) \cdot (xx + y) ^*$ and $\partial_x((xx + y)^*)$.
-To get all the "atomic" components of a regular expression's possible derivatives,
-there is a procedure Antimirov called $\textit{lf}$, short for "linear forms", that takes
-whatever character is available at the head of the string inside the language of a
-regular expression, and gives back the character and the derivative regular expression
-as a pair (which he called "monomial"):
- \begin{center}  
- \begin{tabular}{ccc}
- $\lf(\ONE)$ & $=$ & $\phi$\\
-$\lf(c)$ & $=$ & $\{(c, \ONE) \}$\\
- $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
- $\lf(r^*)$ & $=$ & $\lf(r) \bigodot \lf(r^*)$\\
-\end{tabular}
-\end{center}
-%TODO: completion
-
-There is a slight difference in the last three clauses compared
-with $\partial$: instead of a dot operator $ \textit{rset} \cdot r$ that attaches the regular 
-expression $r$ with every element inside $\textit{rset}$ to create a set of 
-sequence derivatives, it uses the "circle dot" operator $\bigodot$ which operates 
-on a set of monomials (which Antimirov called "linear form") and a regular 
-expression, and returns a linear form:
- \begin{center}  
- \begin{tabular}{ccc}
- $l \bigodot (\ZERO)$ & $=$ & $\phi$\\
- $l \bigodot (\ONE)$ & $=$ & $l$\\
- $\phi \bigodot t$ & $=$ & $\phi$\\
- $\{ (x, \ZERO) \} \bigodot t$ & $=$ & $\{(x,\ZERO) \}$\\
- $\{ (x, \ONE) \} \bigodot t$ & $=$ & $\{(x,t) \}$\\
-  $\{ (x, p) \} \bigodot t$ & $=$ & $\{(x,p\cdot t) \}$\\
- $\lf(a+b)$ & $=$ & $\lf(a) \cup \lf(b)$\\
- $\lf(r^*)$ & $=$ & $\lf(r) \cdot \lf(r^*)$\\
-\end{tabular}
-\end{center}
-%TODO: completion
-
- Some degree of simplification is applied when doing $\bigodot$, for example,
- $l \bigodot (\ZERO) = \phi$ corresponds to $r \cdot \ZERO \rightsquigarrow \ZERO$,
- and  $l \bigodot (\ONE) = l$ to $l \cdot \ONE \rightsquigarrow l$, and
-  $\{ (x, \ZERO) \} \bigodot t = \{(x,\ZERO) \}$ to $\ZERO \cdot x \rightsquigarrow \ZERO$,
-  and so on.
-  
-  With the function $\lf$ one can compute all possible partial derivatives $\partial_{UNIV}(r)$ of a regex $r$ with 
-  an iterative procedure:
-   \begin{center}  
- \begin{tabular}{llll}
-$\textit{while}$ & $(\Delta_i \neq \phi)$  &                &          \\
- 		       &  $\Delta_{i+1}$           &        $ =$ & $\lf(\Delta_i) - \PD_i$ \\
-		       &  $\PD_{i+1}$              &         $ =$ & $\Delta_{i+1} \cup \PD_i$ \\
-$\partial_{UNIV}(r)$ & $=$ & $\PD$ &		     
-\end{tabular}
-\end{center}
-
-
- $(r_1 + r_2) \cdot r_3 \longrightarrow (r_1 \cdot r_3) + (r_2 \cdot r_3)$,
-
-
-However, if we introduce them in our
-setting we would lose the POSIX property of our calculated values. 
-A simple example for this would be the regex $(a + a\cdot b)\cdot(b\cdot c + c)$.
-If we split this regex up into $a\cdot(b\cdot c + c) + a\cdot b \cdot (b\cdot c + c)$, the lexer 
-would give back $\Left(\Seq(\Char(a), \Left(\Char(b \cdot c))))$ instead of
-what we want: $\Seq(\Right(ab), \Right(c))$. Unless we can store the structural information
-in all the places where a transformation of the form $(r_1 + r_2)\cdot r \rightarrow r_1 \cdot r + r_2 \cdot r$
-occurs, and apply them in the right order once we get 
-a result of the "aggressively simplified" regex, it would be impossible to still get a $\POSIX$ value.
-This is unlike the simplification we had before, where the rewriting rules 
-such  as $\ONE \cdot r \rightsquigarrow r$, under which our lexer will give the same value.
-We will discuss better
-bounds in the last section of this chapter.\\[-6.5mm]
-
+We will discuss improvements to this bound in the next chapter.
 
 
 

--- a/ChengsongTanPhdThesis/Chapters/Inj.tex	Wed Aug 31 23:57:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Inj.tex	Thu Sep 01 23:47:37 2022 +0100
@@ -659,10 +659,10 @@
 			\multicolumn{3}{@{}l}{\textbf{Values}}\medskip\\
 			$v$ & $::=$  & \\
 			&        & $\Empty$   \\
-			& $\mid$ & $\Char(c)$          \\
+			& $\mid$ & $\Char \; c$          \\
 			& $\mid$ & $\Seq\,v_1\, v_2$\\
-			& $\mid$ & $\Left(v)$   \\
-			& $\mid$ & $\Right(v)$  \\
+			& $\mid$ & $\Left \;v$   \\
+			& $\mid$ & $\Right\;v$  \\
 			& $\mid$ & $\Stars\,[v_1,\ldots\,v_n]$ \\
 		\end{tabular}
 	\end{tabular}
@@ -674,28 +674,28 @@
 	\begin{tabular}{lcl}
 		$|\Empty|$ & $\dn$ &  $[]$\\
 		$|\Char \; c|$ & $ \dn$ & $ [c]$\\
-		$|\Seq(v_1, v_2)|$ & $ \dn$ & $ v_1| @ |v_2|$\\
-		$|\Left(v)|$ & $ \dn$ & $ |v|$\\
-		$|\Right(v)|$ & $ \dn$ & $ |v|$\\
-		$|\Stars([])|$ & $\dn$ & $[]$\\
-		$|\Stars(v::vs)|$ &  $\dn$ & $ |v| @ |\Stars(vs)|$
+		$|\Seq \; v_1, \;v_2|$ & $ \dn$ & $ v_1| @ |v_2|$\\
+		$|\Left \; v|$ & $ \dn$ & $ |v|$\\
+		$|\Right \; v|$ & $ \dn$ & $ |v|$\\
+		$|\Stars \; []|$ & $\dn$ & $[]$\\
+		$|\Stars \; v::vs|$ &  $\dn$ & $ |v| @ |\Stars(vs)|$
 	\end{tabular}
 \end{center}
 Sulzmann and Lu used a binary predicate, written $\vdash v:r $,
 to indicate that a value $v$ could be generated from a lexing algorithm
 with input $r$. They call it the value inhabitation relation. 
 \begin{mathpar}
-	\inferrule{\mbox{}}{\vdash \Char(c) : \mathbf{c}} \hspace{2em}
+	\inferrule{\mbox{}}{\vdash \Char \; c : \mathbf{c}} \hspace{2em}
 
 	\inferrule{\mbox{}}{\vdash \Empty :  \ONE} \hspace{2em}
 
-\inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq(v_1, v_2) : (r_1 \cdot r_2)}
+\inferrule{\vdash v_1 : r_1 \;\; \vdash v_2 : r_2 }{\vdash \Seq \; v_1,\; v_2 : (r_1 \cdot r_2)}
 
-\inferrule{\vdash v_1 : r_1}{\vdash \Left(v_1):r_1+r_2}
+\inferrule{\vdash v_1 : r_1}{\vdash \Left \; v_1 : r_1+r_2}
 
-\inferrule{\vdash v_2 : r_2}{\vdash \Right(v_2):r_1 + r_2}
+\inferrule{\vdash v_2 : r_2}{\vdash \Right \; v_2:r_1 + r_2}
 
-\inferrule{\forall v \in vs. \vdash v:r \land  |v| \neq []}{\vdash \Stars(vs):r^*}
+\inferrule{\forall v \in vs. \vdash v:r \land  |v| \neq []}{\vdash \Stars \; vs : r^*}
 \end{mathpar}
 \noindent
 The condition $|v| \neq []$ in the premise of star's rule

--- a/ChengsongTanPhdThesis/Chapters/Introduction.tex	Wed Aug 31 23:57:42 2022 +0100
+++ b/ChengsongTanPhdThesis/Chapters/Introduction.tex	Thu Sep 01 23:47:37 2022 +0100
@@ -25,6 +25,7 @@
 \def\rders{\textit{rders}}
 \newcommand{\bders}[2]{#1 \backslash #2}
 \newcommand{\bsimp}[1]{\textit{bsimp}(#1)}
+\def\bsimps{\textit{bsimp}}
 \newcommand{\rsimp}[1]{\textit{rsimp}\; #1}
 \newcommand{\sflataux}[1]{\llparenthesis #1 \rrparenthesis'}
 \newcommand{\dn}{\stackrel{\mbox{\scriptsize def}}{=}}%
@@ -119,7 +120,7 @@
 \def\blexersimp{\mathit{blexer}\_\mathit{simp}}
 \def\blexerStrong{\textit{blexerStrong}}
 \def\bsimpStrong{\textit{bsimpStrong}}
-%\def\bdersStrong{\textit{bdersStrong}}
+\def\bdersStrongs{\textit{bdersStrong}}
 \newcommand{\bdersStrong}[2]{#1 \backslash_{bsimpStrongs} #2}
 
 \def\map{\textit{map}}

--- a/thys2/blexer2.sc	Wed Aug 31 23:57:42 2022 +0100
+++ b/thys2/blexer2.sc	Thu Sep 01 23:47:37 2022 +0100
@@ -28,8 +28,8 @@
 case class NTIMES(n: Int, r: Rexp) extends Rexp
 case class OPTIONAL(r: Rexp) extends Rexp
 case class NOT(r: Rexp) extends Rexp
-                // records for extracting strings or tokens
-  
+// records for extracting strings or tokens
+
 // values  
 abstract class Val
 case object Failure extends Val
@@ -66,12 +66,12 @@
 import scala.util.Try
 
 trait Generator[+T] {
-    self => // an alias for "this"
+  self => // an alias for "this"
     def generate(): T
-  
+
     def gen(n: Int) : List[T] = 
       if (n == 0) Nil else self.generate() :: gen(n - 1)
-    
+
     def map[S](f: T => S): Generator[S] = new Generator[S] {
       def generate = f(self.generate())  
     }
@@ -82,22 +82,22 @@
 
 }
 
-  // tests a property according to a given random generator
-  def test[T](r: Generator[T], amount: Int = 100)(pred: T => Boolean) {
-    for (_ <- 0 until amount) {
-      val value = r.generate()
-      assert(pred(value), s"Test failed for: $value")
-    }
-    println(s"Test passed $amount times")
+// tests a property according to a given random generator
+def test[T](r: Generator[T], amount: Int = 100)(pred: T => Boolean) {
+  for (_ <- 0 until amount) {
+    val value = r.generate()
+    assert(pred(value), s"Test failed for: $value")
   }
-  def test2[T, S](r: Generator[T], s: Generator[S], amount: Int = 100)(pred: (T, S) => Boolean) {
-    for (_ <- 0 until amount) {
-      val valueR = r.generate()
-      val valueS = s.generate()
-      assert(pred(valueR, valueS), s"Test failed for: $valueR, $valueS")
-    }
-    println(s"Test passed $amount times")
+  println(s"Test passed $amount times")
+}
+def test2[T, S](r: Generator[T], s: Generator[S], amount: Int = 100)(pred: (T, S) => Boolean) {
+  for (_ <- 0 until amount) {
+    val valueR = r.generate()
+    val valueS = s.generate()
+    assert(pred(valueR, valueS), s"Test failed for: $valueR, $valueS")
   }
+  println(s"Test passed $amount times")
+}
 
 // random integers
 val integers = new Generator[Int] {
@@ -107,7 +107,7 @@
 
 // random booleans
 val booleans = integers.map(_ > 0)
-  
+
 // random integers in the range lo and high  
 def range(lo: Int, hi: Int): Generator[Int] = 
   for (x <- integers) yield (lo + x.abs % (hi - lo)).abs
@@ -119,7 +119,7 @@
 
 def oneOf[T](xs: T*): Generator[T] = 
   for (idx <- range(0, xs.length)) yield xs(idx)
-  
+
 def single[T](x: T) = new Generator[T] {
   def generate() = x
 }   
@@ -185,22 +185,22 @@
 def leaf_rexp() : Generator[Rexp] =
   for (kind <- range(0, 5);
        c <- chars_range('a', 'd')) yield
-    kind match {
-      case 0 => ZERO
-      case 1 => ONE
-      case _ => CHAR(c) 
-    }
+kind match {
+  case 0 => ZERO
+  case 1 => ONE
+  case _ => CHAR(c) 
+}
 
 // generates random inner regexes with maximum depth d
 def inner_rexp(d: Int) : Generator[Rexp] =
   for (kind <- range(0, 3);
        l <- rexp(d); 
        r <- rexp(d))
-  yield kind match {
-    case 0 => ALTS(l, r)
-    case 1 => SEQ(l, r)
-    case 2 => STAR(r)
-  }
+yield kind match {
+  case 0 => ALTS(l, r)
+  case 1 => SEQ(l, r)
+  case 2 => STAR(r)
+}
 
 // generates random regexes with maximum depth d;
 // prefers inner regexes in 2/3 of the cases
@@ -239,7 +239,7 @@
 }
 
 
-   
+
 // some convenience for typing in regular expressions
 
 def charlist2rexp(s : List[Char]): Rexp = s match {
@@ -250,209 +250,209 @@
 implicit def string2rexp(s : String) : Rexp = 
   charlist2rexp(s.toList)
 
-implicit def RexpOps(r: Rexp) = new {
-  def | (s: Rexp) = ALTS(r, s)
-  def % = STAR(r)
-  def ~ (s: Rexp) = SEQ(r, s)
-}
+  implicit def RexpOps(r: Rexp) = new {
+    def | (s: Rexp) = ALTS(r, s)
+    def % = STAR(r)
+    def ~ (s: Rexp) = SEQ(r, s)
+  }
 
-implicit def stringOps(s: String) = new {
-  def | (r: Rexp) = ALTS(s, r)
-  def | (r: String) = ALTS(s, r)
-  def % = STAR(s)
-  def ~ (r: Rexp) = SEQ(s, r)
-  def ~ (r: String) = SEQ(s, r)
-  def $ (r: Rexp) = RECD(s, r)
-}
+  implicit def stringOps(s: String) = new {
+    def | (r: Rexp) = ALTS(s, r)
+    def | (r: String) = ALTS(s, r)
+    def % = STAR(s)
+    def ~ (r: Rexp) = SEQ(s, r)
+    def ~ (r: String) = SEQ(s, r)
+    def $ (r: Rexp) = RECD(s, r)
+  }
 
-def nullable(r: Rexp) : Boolean = r match {
-  case ZERO => false
-  case ONE => true
-  case CHAR(_) => false
-  case ANYCHAR => false
-  case ALTS(r1, r2) => nullable(r1) || nullable(r2)
-  case ALTSS(rs) => rs.exists(nullable)
-  case SEQ(r1, r2) => nullable(r1) && nullable(r2)
-  case STAR(_) => true
-  case RECD(_, r1) => nullable(r1)
-  case NTIMES(n, r) => if (n == 0) true else nullable(r)
-  case OPTIONAL(r) => true
-  case NOT(r) => !nullable(r)
-}
+  def nullable(r: Rexp) : Boolean = r match {
+    case ZERO => false
+    case ONE => true
+    case CHAR(_) => false
+    case ANYCHAR => false
+    case ALTS(r1, r2) => nullable(r1) || nullable(r2)
+    case ALTSS(rs) => rs.exists(nullable)
+    case SEQ(r1, r2) => nullable(r1) && nullable(r2)
+    case STAR(_) => true
+    case RECD(_, r1) => nullable(r1)
+    case NTIMES(n, r) => if (n == 0) true else nullable(r)
+    case OPTIONAL(r) => true
+    case NOT(r) => !nullable(r)
+  }
 
-def der(c: Char, r: Rexp) : Rexp = r match {
-  case ZERO => ZERO
-  case ONE => ZERO
-  case CHAR(d) => if (c == d) ONE else ZERO
-  case ANYCHAR => ONE 
-  case ALTS(r1, r2) => ALTS(der(c, r1), der(c, r2))
-  case ALTSS(rs) => ALTSS(rs.map(der(c, _)))
-  case SEQ(r1, r2) => 
-    if (nullable(r1)) ALTS(SEQ(der(c, r1), r2), der(c, r2))
-    else SEQ(der(c, r1), r2)
-  case STAR(r) => SEQ(der(c, r), STAR(r))
-  case RECD(_, r1) => der(c, r1)
-  case NTIMES(n, r) => if(n > 0) SEQ(der(c, r), NTIMES(n - 1, r)) else ZERO
-  case OPTIONAL(r) => der(c, r)
-  case NOT(r) =>  NOT(der(c, r))
-}
+  def der(c: Char, r: Rexp) : Rexp = r match {
+    case ZERO => ZERO
+    case ONE => ZERO
+    case CHAR(d) => if (c == d) ONE else ZERO
+    case ANYCHAR => ONE 
+    case ALTS(r1, r2) => ALTS(der(c, r1), der(c, r2))
+    case ALTSS(rs) => ALTSS(rs.map(der(c, _)))
+    case SEQ(r1, r2) => 
+      if (nullable(r1)) ALTS(SEQ(der(c, r1), r2), der(c, r2))
+      else SEQ(der(c, r1), r2)
+    case STAR(r) => SEQ(der(c, r), STAR(r))
+    case RECD(_, r1) => der(c, r1)
+    case NTIMES(n, r) => if(n > 0) SEQ(der(c, r), NTIMES(n - 1, r)) else ZERO
+    case OPTIONAL(r) => der(c, r)
+    case NOT(r) =>  NOT(der(c, r))
+  }
 
-def ders(s: List[Char], r: Rexp) : Rexp = s match {
-  case Nil => r
-  case c :: cs => ders(cs, der(c, r))
-}
+  def ders(s: List[Char], r: Rexp) : Rexp = s match {
+    case Nil => r
+    case c :: cs => ders(cs, der(c, r))
+  }
 
-def ders_simp(s: List[Char], r: Rexp) : Rexp = s match {
-  case Nil => simp(r)
-  case c :: cs => ders_simp(cs, simp(der(c, r)))
-}
+  def ders_simp(s: List[Char], r: Rexp) : Rexp = s match {
+    case Nil => simp(r)
+    case c :: cs => ders_simp(cs, simp(der(c, r)))
+  }
 
 
-def simp2(r: Rexp) : Rexp = r match {
-  case SEQ(r1, r2) => 
-    (simp2(r1), simp2(r2)) match {
-      case (ZERO, _) => ZERO
-      case (_, ZERO) => ZERO
-      case (ONE, r2s) => r2s
-      case (r1s, ONE) => r1s
-      case (r1s, r2s) => 
-        SEQ(r1s, r2s)
-    }
-  case ALTS(r1, r2) => 
-    val r1r2s = fltsplain(simp2(r1) :: simp2(r2) :: Nil).distinct 
-    r1r2s match {
-      case Nil => ZERO
-      case r :: Nil => r
-      case r1 :: r2 :: rs => 
-        ALTSS(r1 :: r2 :: rs)
-    }
-  case ALTSS(rs) => 
-    // println(rs)
-    (fltsplain(rs.map(simp2))).distinct match {
-      case Nil => ZERO
-      case r :: Nil => r
-      case r1 :: r2 :: rs =>
-        ALTSS(r1 :: r2 :: rs)
-    }
-  case r => r
-}
+  def simp2(r: Rexp) : Rexp = r match {
+    case SEQ(r1, r2) => 
+      (simp2(r1), simp2(r2)) match {
+        case (ZERO, _) => ZERO
+        case (_, ZERO) => ZERO
+        case (ONE, r2s) => r2s
+        case (r1s, ONE) => r1s
+        case (r1s, r2s) => 
+          SEQ(r1s, r2s)
+      }
+        case ALTS(r1, r2) => 
+          val r1r2s = fltsplain(simp2(r1) :: simp2(r2) :: Nil).distinct 
+          r1r2s match {
+            case Nil => ZERO
+            case r :: Nil => r
+            case r1 :: r2 :: rs => 
+              ALTSS(r1 :: r2 :: rs)
+          }
+            case ALTSS(rs) => 
+              // println(rs)
+              (fltsplain(rs.map(simp2))).distinct match {
+                case Nil => ZERO
+                case r :: Nil => r
+                case r1 :: r2 :: rs =>
+                  ALTSS(r1 :: r2 :: rs)
+              }
+                case r => r
+  }
 
 
-def simp(r: Rexp) : Rexp = r match {
-  case SEQ(r1, r2) => 
-    (simp(r1), simp(r2)) match {
-      case (ZERO, _) => ZERO
-      case (_, ZERO) => ZERO
-      case (ONE, r2s) => r2s
-      case (r1s, ONE) => r1s
-      case (r1s, r2s) => SEQ(r1s, r2s)
-    }
-  case ALTS(r1, r2) => {
-    (simp(r1), simp(r2)) match {
-      case (ZERO, r2s) => r2s
-      case (r1s, ZERO) => r1s
-      case (r1s, r2s) =>
-        if(r1s == r2s) r1s else ALTS(r1s, r2s)
-    }
+  def simp(r: Rexp) : Rexp = r match {
+    case SEQ(r1, r2) => 
+      (simp(r1), simp(r2)) match {
+        case (ZERO, _) => ZERO
+        case (_, ZERO) => ZERO
+        case (ONE, r2s) => r2s
+        case (r1s, ONE) => r1s
+        case (r1s, r2s) => SEQ(r1s, r2s)
+      }
+        case ALTS(r1, r2) => {
+          (simp(r1), simp(r2)) match {
+            case (ZERO, r2s) => r2s
+            case (r1s, ZERO) => r1s
+            case (r1s, r2s) =>
+              if(r1s == r2s) r1s else ALTS(r1s, r2s)
+          }
+        }
+            case r => r
   }
-  case r => r
-}
 
-def fltsplain(rs: List[Rexp]) : List[Rexp] = rs match {
-  case Nil => Nil
-  case ZERO :: rs => fltsplain(rs)
-  case ALTS(r1, r2) :: rs => r1 :: r2 :: fltsplain(rs) 
-  case ALTSS(rs) :: rs1 => rs ::: fltsplain(rs1)
-  case r :: rs => r :: fltsplain(rs)
-}
+  def fltsplain(rs: List[Rexp]) : List[Rexp] = rs match {
+    case Nil => Nil
+    case ZERO :: rs => fltsplain(rs)
+    case ALTS(r1, r2) :: rs => r1 :: r2 :: fltsplain(rs) 
+    case ALTSS(rs) :: rs1 => rs ::: fltsplain(rs1)
+    case r :: rs => r :: fltsplain(rs)
+  }
 
 
 
 
-def matcher(s: String, r: Rexp) : Boolean = 
-  nullable(ders(s.toList, r))
+  def matcher(s: String, r: Rexp) : Boolean = 
+    nullable(ders(s.toList, r))
 
-def simp_matcher(s: String, r: Rexp) : Boolean = 
-  nullable(ders_simp(s.toList, r))
+  def simp_matcher(s: String, r: Rexp) : Boolean = 
+    nullable(ders_simp(s.toList, r))
 
 
-// extracts a string from a value
-def flatten(v: Val) : String = v match {
-  case Empty => ""
-  case Chr(c) => c.toString
-  case Left(v) => flatten(v)
-  case Right(v) => flatten(v)
-  case Sequ(v1, v2) => flatten(v1) ++ flatten(v2)
-  case Stars(vs) => vs.map(flatten).mkString
-  case Ntime(vs) => vs.map(flatten).mkString
-  case Optionall(v) => flatten(v)
-  case Rec(_, v) => flatten(v)
-}
+  // extracts a string from a value
+  def flatten(v: Val) : String = v match {
+    case Empty => ""
+    case Chr(c) => c.toString
+    case Left(v) => flatten(v)
+    case Right(v) => flatten(v)
+    case Sequ(v1, v2) => flatten(v1) ++ flatten(v2)
+    case Stars(vs) => vs.map(flatten).mkString
+    case Ntime(vs) => vs.map(flatten).mkString
+    case Optionall(v) => flatten(v)
+    case Rec(_, v) => flatten(v)
+  }
 
 
-// extracts an environment from a value;
-// used for tokenising a string
-def env(v: Val) : List[(String, String)] = v match {
-  case Empty => Nil
-  case Chr(c) => Nil
-  case Left(v) => env(v)
-  case Right(v) => env(v)
-  case Sequ(v1, v2) => env(v1) ::: env(v2)
-  case Stars(vs) => vs.flatMap(env)
-  case Ntime(vs) => vs.flatMap(env)
-  case Rec(x, v) => (x, flatten(v))::env(v)
-  case Optionall(v) => env(v)
-  case Nots(s) => ("Negative", s) :: Nil
-}
+  // extracts an environment from a value;
+  // used for tokenising a string
+  def env(v: Val) : List[(String, String)] = v match {
+    case Empty => Nil
+    case Chr(c) => Nil
+    case Left(v) => env(v)
+    case Right(v) => env(v)
+    case Sequ(v1, v2) => env(v1) ::: env(v2)
+    case Stars(vs) => vs.flatMap(env)
+    case Ntime(vs) => vs.flatMap(env)
+    case Rec(x, v) => (x, flatten(v))::env(v)
+    case Optionall(v) => env(v)
+    case Nots(s) => ("Negative", s) :: Nil
+  }
 
 
-// The injection and mkeps part of the lexer
-//===========================================
+  // The injection and mkeps part of the lexer
+  //===========================================
 
-def mkeps(r: Rexp) : Val = r match {
-  case ONE => Empty
-  case ALTS(r1, r2) => 
-    if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2))
-  case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2))
-  case STAR(r) => Stars(Nil)
-  case RECD(x, r) => Rec(x, mkeps(r))
-  case NTIMES(n, r) => Ntime(List.fill(n)(mkeps(r)))
-  case OPTIONAL(r) => Optionall(Empty)
-  case NOT(rInner) => if(nullable(rInner)) throw new Exception("error")  
-                         else Nots("")//Nots(s.reverse.toString)
-//   case NOT(ZERO) => Empty
-//   case NOT(CHAR(c)) => Empty
-//   case NOT(SEQ(r1, r2)) => Sequ(mkeps(NOT(r1)), mkeps(NOT(r2)))
-//   case NOT(ALTS(r1, r2)) => if(!nullable(r1)) Left(mkeps(NOT(r1))) else Right(mkeps(NOT(r2)))
-//   case NOT(STAR(r)) => Stars(Nil) 
+  def mkeps(r: Rexp) : Val = r match {
+    case ONE => Empty
+    case ALTS(r1, r2) => 
+      if (nullable(r1)) Left(mkeps(r1)) else Right(mkeps(r2))
+    case SEQ(r1, r2) => Sequ(mkeps(r1), mkeps(r2))
+    case STAR(r) => Stars(Nil)
+    case RECD(x, r) => Rec(x, mkeps(r))
+    case NTIMES(n, r) => Ntime(List.fill(n)(mkeps(r)))
+    case OPTIONAL(r) => Optionall(Empty)
+    case NOT(rInner) => if(nullable(rInner)) throw new Exception("error")  
+    else Nots("")//Nots(s.reverse.toString)
+    //   case NOT(ZERO) => Empty
+    //   case NOT(CHAR(c)) => Empty
+    //   case NOT(SEQ(r1, r2)) => Sequ(mkeps(NOT(r1)), mkeps(NOT(r2)))
+    //   case NOT(ALTS(r1, r2)) => if(!nullable(r1)) Left(mkeps(NOT(r1))) else Right(mkeps(NOT(r2)))
+    //   case NOT(STAR(r)) => Stars(Nil) 
 
-}
+  }
 
-def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
-  case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs)
-  case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2)
-  case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2)
-  case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
-  case (ALTS(r1, r2), Left(v1)) => Left(inj(r1, c, v1))
-  case (ALTS(r1, r2), Right(v2)) => Right(inj(r2, c, v2))
-  case (CHAR(d), Empty) => Chr(c) 
-  case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
-  case (NTIMES(n, r), Sequ(v1, Ntime(vs))) => Ntime(inj(r, c, v1)::vs)
-  case (OPTIONAL(r), v) => Optionall(inj(r, c, v))
-  case (NOT(r), Nots(s)) => Nots(c.toString ++ s)
-  case (ANYCHAR, Empty) => Chr(c)
-}
+  def inj(r: Rexp, c: Char, v: Val) : Val = (r, v) match {
+    case (STAR(r), Sequ(v1, Stars(vs))) => Stars(inj(r, c, v1)::vs)
+    case (SEQ(r1, r2), Sequ(v1, v2)) => Sequ(inj(r1, c, v1), v2)
+    case (SEQ(r1, r2), Left(Sequ(v1, v2))) => Sequ(inj(r1, c, v1), v2)
+    case (SEQ(r1, r2), Right(v2)) => Sequ(mkeps(r1), inj(r2, c, v2))
+    case (ALTS(r1, r2), Left(v1)) => Left(inj(r1, c, v1))
+    case (ALTS(r1, r2), Right(v2)) => Right(inj(r2, c, v2))
+    case (CHAR(d), Empty) => Chr(c) 
+    case (RECD(x, r1), _) => Rec(x, inj(r1, c, v))
+    case (NTIMES(n, r), Sequ(v1, Ntime(vs))) => Ntime(inj(r, c, v1)::vs)
+    case (OPTIONAL(r), v) => Optionall(inj(r, c, v))
+    case (NOT(r), Nots(s)) => Nots(c.toString ++ s)
+    case (ANYCHAR, Empty) => Chr(c)
+  }
 
-// some "rectification" functions for simplification
+  // some "rectification" functions for simplification
 
 
 
 
-// The Lexing Rules for the WHILE Language
+  // The Lexing Rules for the WHILE Language
 
   // bnullable function: tests whether the aregular 
   // expression can recognise the empty string
-def bnullable (r: ARexp) : Boolean = r match {
+  def bnullable (r: ARexp) : Boolean = r match {
     case AZERO => false
     case AONE(_) => true
     case ACHAR(_,_) => false
@@ -462,7 +462,7 @@
     case ANOT(_, rn) => !bnullable(rn)
   }
 
-def mkepsBC(r: ARexp) : Bits = r match {
+  def mkepsBC(r: ARexp) : Bits = r match {
     case AONE(bs) => bs
     case AALTS(bs, rs) => {
       val n = rs.indexWhere(bnullable)
@@ -474,7 +474,7 @@
   }
 
 
-def bder(c: Char, r: ARexp) : ARexp = r match {
+  def bder(c: Char, r: ARexp) : ARexp = r match {
     case AZERO => AZERO
     case AONE(_) => AZERO
     case ACHAR(bs, f) => if (c == f) AONE(bs) else AZERO
@@ -487,7 +487,7 @@
     case AANYCHAR(bs) => AONE(bs)
   } 
 
-def fuse(bs: Bits, r: ARexp) : ARexp = r match {
+  def fuse(bs: Bits, r: ARexp) : ARexp = r match {
     case AZERO => AZERO
     case AONE(cs) => AONE(bs ++ cs)
     case ACHAR(cs, f) => ACHAR(bs ++ cs, f)
@@ -498,17 +498,17 @@
   }
 
 
-def internalise(r: Rexp) : ARexp = r match {
+  def internalise(r: Rexp) : ARexp = r match {
     case ZERO => AZERO
     case ONE => AONE(Nil)
     case CHAR(c) => ACHAR(Nil, c)
     //case PRED(f) => APRED(Nil, f)
     case ALTS(r1, r2) => 
       AALTS(Nil, List(fuse(List(Z), internalise(r1)), fuse(List(S), internalise(r2))))
-    // case ALTS(r1::rs) => {
-    //   val AALTS(Nil, rs2) = internalise(ALTS(rs))
-    //   AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _)))
-    // }
+      // case ALTS(r1::rs) => {
+      //   val AALTS(Nil, rs2) = internalise(ALTS(rs))
+      //   AALTS(Nil, fuse(List(Z), internalise(r1)) :: rs2.map(fuse(List(S), _)))
+      // }
     case SEQ(r1, r2) => ASEQ(Nil, internalise(r1), internalise(r2))
     case STAR(r) => ASTAR(Nil, internalise(r))
     case RECD(x, r) => internalise(r)
@@ -517,39 +517,39 @@
   }
 
 
-def bsimp(r: ARexp): ARexp = 
+  def bsimp(r: ARexp): ARexp = 
   {
     r match {
       case ASEQ(bs1, r1, r2) => (bsimp(r1), bsimp(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) => {
-            val rs_simp = rs.map(bsimp(_))
-            val flat_res = flats(rs_simp)
-            val dist_res = distinctBy(flat_res, erase)//strongDB(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 strongBsimp(r: ARexp): ARexp =
-{
-  r match {
-    case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(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) => {
+          val rs_simp = rs.map(bsimp(_))
+          val flat_res = flats(rs_simp)
+          val dist_res = distinctBy(flat_res, erase)//strongDB(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
     }
-    case AALTS(bs1, rs) => {
+  }
+  def strongBsimp(r: ARexp): ARexp =
+  {
+    r match {
+      case ASEQ(bs1, r1, r2) => (strongBsimp(r1), strongBsimp(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) => {
           val rs_simp = rs.map(strongBsimp(_))
           val flat_res = flats(rs_simp)
           val dist_res = distinctBy4(flat_res)//distinctBy(flat_res, erase)
@@ -558,24 +558,24 @@
             case s :: Nil => fuse(bs1, s)
             case rs => AALTS(bs1, rs)  
           }
-        
+
+        }
+            case r => r
     }
-    case r => r
   }
-}
 
-def strongBsimp5(r: ARexp): ARexp =
-{
-  // println("was this called?")
-  r match {
-    case ASEQ(bs1, r1, r2) => (strongBsimp5(r1), strongBsimp5(r2)) match {
+  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")
+      }
+        case AALTS(bs1, rs) => {
+          // println("alts case")
           val rs_simp = rs.map(strongBsimp5(_))
           val flat_res = flats(rs_simp)
           var dist_res = distinctBy5(flat_res)//distinctBy(flat_res, erase)
@@ -589,25 +589,25 @@
             case s :: Nil => fuse(bs1, s)
             case rs => AALTS(bs1, rs)  
           }
+        }
+            case r => r
     }
-    case r => r
   }
-}
 
-def strongBsimp6(r: ARexp): ARexp =
-{
-  // println("was this called?")
-  r match {
-    case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(r2)) match {
+  def strongBsimp6(r: ARexp): ARexp =
+  {
+    // println("was this called?")
+    r match {
+      case ASEQ(bs1, r1, r2) => (strongBsimp6(r1), strongBsimp6(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")
+      }
+        case AALTS(bs1, rs) => {
+          // println("alts case")
           val rs_simp = rs.map(strongBsimp6(_))
           val flat_res = flats(rs_simp)
           var dist_res = distinctBy6(flat_res)//distinctBy(flat_res, erase)
@@ -616,745 +616,746 @@
             case s :: Nil => fuse(bs1, s)
             case rs => AALTS(bs1, rs)  
           }
+        }
+        //(erase(r0))) => AONE(bs)
+            case r => r
     }
-    //(erase(r0))) => AONE(bs)
-    case r => r
-  }
-}
-
-def distinctWith(rs: List[ARexp], 
-                pruneFunction: (ARexp, Set[Rexp]) => ARexp, 
-                acc: Set[Rexp] = Set()) : List[ARexp] = 
-  rs match{
-    case Nil => Nil
-    case r :: rs => 
-      if(acc(erase(r)))
-        distinctWith(rs, pruneFunction, acc)
-      else {
-        val pruned_r = pruneFunction(r, acc)
-        pruned_r :: 
-        distinctWith(rs, 
-          pruneFunction, 
-          turnIntoTerms(erase(pruned_r)) ++: acc
-        )
-      }
   }
 
-// def distinctByPlus(rs: List[ARexp], acc: Set[Rexp] = Set()) : 
-// List[ARexp] =  rs match {
-//   case Nil => Nil
-//   case r :: rs =>
-//     if(acc.contains(erase(r)))
-//       distinctByPlus(rs, acc)
-//     else 
-//       prune(r, acc) :: distinctByPlus(rs, prune(r, acc) +: acc)
-// }
+
+    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
+    }
+
 
-//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 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 distinctWith(rs: List[ARexp], 
+    pruneFunction: (ARexp, Set[Rexp]) => ARexp, 
+    acc: Set[Rexp] = Set()) : List[ARexp] = 
+      rs match{
+        case Nil => Nil
+        case r :: rs => 
+          if(acc(erase(r)))
+            distinctWith(rs, pruneFunction, acc)
+          else {
+            val pruned_r = pruneFunction(r, acc)
+            pruned_r :: 
+            distinctWith(rs, 
+              pruneFunction, 
+              turnIntoTerms(erase(pruned_r)) ++: acc
+              )
+          }
+      }
 
-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
-}
+    //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 strongBsimp7(r: ARexp): ARexp =
-{
-  r match {
-    case ASEQ(bs1, r1, r2) => (strongBsimp7(r1), strongBsimp7(r2)) match {
+    def prune(r: ARexp, acc: Set[Rexp]) : ARexp = r match{
+      case AALTS(bs, rs) => rs.map(r => prune(r, acc)).filter(_ != ZERO) match
+      {
+        //all components have been removed, meaning this is effectively a duplicate
+        //flats will take care of removing this AZERO 
+        case Nil => AZERO
+        case r::Nil => fuse(bs, r)
+        case rs1 => AALTS(bs, rs1)
+      }
+      case ASEQ(bs, r1, r2) => 
+        //remove the r2 in (ra + rb)r2 to identify the duplicate contents of r1
+        prune(r1, acc.map(r => removeSeqTail(r, erase(r2)))) match {
+          //after pruning, returns 0
+          case AZERO => AZERO
+          //after pruning, got r1'.r2, where r1' is equal to 1
+          case r1p if(isOne(erase(r1p))) => fuse(bs ++ mkepsBC(r1p), r2)
+          //assemble the pruned head r1p with r2
+          case r1p => ASEQ(bs, r1p, r2)
+        }
+        //this does the duplicate component removal task
+      case r => if(acc(erase(r))) AZERO else r
+    }
+
+    //a stronger version of simp
+    def bsimpStrong(r: ARexp): ARexp =
+    {
+      r match {
+        case ASEQ(bs1, r1, r2) => (bsimpStrong(r1), bsimpStrong(r2)) match {
+          //normal clauses same as simp
         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)
+        //bs2 can be discarded
+        case (r1s, AONE(bs2)) => fuse(bs1, r1s) //assert bs2 == Nil
         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 AALTS(bs1, rs) => {
+          //distinctBy(flat_res, erase)
+          distinctWith(flats(rs.map(bsimpStrong(_))), prune) match {
             case Nil => AZERO
             case s :: Nil => fuse(bs1, s)
             case rs => AALTS(bs1, rs)  
           }
+        }
+        //stars that can be treated as 1
+        case ASTAR(bs, r0) if(atMostEmpty(erase(r0))) => AONE(bs)
+        case r => r
+      }
     }
-    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))
-}
-
-def flats(rs: List[ARexp]): List[ARexp] = rs match {
-    case Nil => Nil
-    case AZERO :: rs1 => flats(rs1)
-    case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
-    case r1 :: rs2 => r1 :: flats(rs2)
-  }
-
-def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
-  case Nil => Nil
-  case (x::xs) => {
-    val res = f(x)
-    if (acc.contains(res)) distinctBy(xs, f, acc)  
-    else x::distinctBy(xs, f, res::acc)
-  }
-} 
 
 
-def pruneRexp(r: ARexp, allowableTerms: List[Rexp]) : ARexp = {
-  r match {
-    case ASEQ(bs, r1, r2) => 
-      val termsTruncated = allowableTerms.collect(rt => rt match {
-        case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2)) 
-      })
-      val pruned : ARexp = pruneRexp(r1, termsTruncated)
-      pruned match {
-        case AZERO => AZERO
-        case AONE(bs1) => fuse(bs ++ bs1, r2)
-        case pruned1 => ASEQ(bs, pruned1, r2)
-      }
+    def bders (s: List[Char], r: ARexp) : ARexp = s match {
+      case Nil => r
+      case c::s => bders(s, bder(c, r))
+    }
 
-    case AALTS(bs, rs) => 
-      //allowableTerms.foreach(a => println(shortRexpOutput(a)))        
-      val rsp = rs.map(r => 
-                    pruneRexp(r, allowableTerms)
-                  )
-                  .filter(r => r != AZERO)
-      rsp match {
-        case Nil => AZERO
-        case r1::Nil => fuse(bs, r1)
-        case rs1 => AALTS(bs, rs1)
+    def flats(rs: List[ARexp]): List[ARexp] = rs match {
+      case Nil => Nil
+      case AZERO :: rs1 => flats(rs1)
+      case AALTS(bs, rs1) :: rs2 => rs1.map(fuse(bs, _)) ::: flats(rs2)
+      case r1 :: rs2 => r1 :: flats(rs2)
+    }
+
+    def distinctBy[B, C](xs: List[B], f: B => C, acc: List[C] = Nil): List[B] = xs match {
+      case Nil => Nil
+      case (x::xs) => {
+        val res = f(x)
+        if (acc.contains(res)) distinctBy(xs, f, acc)  
+        else x::distinctBy(xs, f, res::acc)
       }
-    case r => 
-      if(allowableTerms.contains(erase(r))) r else AZERO //assert(r != AZERO)
-  }
-}
-
-def oneSimp(r: Rexp) : Rexp = r match {
-  case SEQ(ONE, r) => r
-  case SEQ(r1, r2) => SEQ(oneSimp(r1), r2)
-  case r => r//assert r != 0 
-    
-}
+    } 
 
 
-def distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
-  case Nil => Nil
-  case x :: xs =>
-    //assert(acc.distinct == acc)
-    val erased = erase(x)
-    if(acc.contains(erased))
-      distinctBy4(xs, acc)
-    else{
-      val addToAcc =  breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
-      //val xp = pruneRexp(x, addToAcc)
-      pruneRexp(x, addToAcc) match {
-        case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
-        case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
+    def pruneRexp(r: ARexp, allowableTerms: List[Rexp]) : ARexp = {
+      r match {
+        case ASEQ(bs, r1, r2) => 
+          val termsTruncated = allowableTerms.collect(rt => rt match {
+            case SEQ(r1p, r2p) if(r2p == erase(r2)) => r1p//if(r2p == erase(r2)) 
+          })
+          val pruned : ARexp = pruneRexp(r1, termsTruncated)
+          pruned match {
+            case AZERO => AZERO
+            case AONE(bs1) => fuse(bs ++ bs1, r2)
+            case pruned1 => ASEQ(bs, pruned1, r2)
+          }
+
+            case AALTS(bs, rs) => 
+              //allowableTerms.foreach(a => println(shortRexpOutput(a)))        
+              val rsp = rs.map(r => 
+                  pruneRexp(r, allowableTerms)
+                  )
+                    .filter(r => r != AZERO)
+                    rsp match {
+                      case Nil => AZERO
+                      case r1::Nil => fuse(bs, r1)
+                      case rs1 => AALTS(bs, rs1)
+                    }
+                      case r => 
+                        if(allowableTerms.contains(erase(r))) r else AZERO //assert(r != AZERO)
       }
     }
-}
+
+    def oneSimp(r: Rexp) : Rexp = r match {
+      case SEQ(ONE, r) => r
+      case SEQ(r1, r2) => SEQ(oneSimp(r1), r2)
+      case r => r//assert r != 0 
+
+    }
+
 
-// fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
-//   where
-// "pAKC_aux rsa r ctx = (if (seqFold (SEQ (erase r) ( ctx) )) ⊆ (seqFold (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 distinctBy4(xs: List[ARexp], acc: List[Rexp] = Nil) : List[ARexp] = xs match {
+      case Nil => Nil
+      case x :: xs =>
+        //assert(acc.distinct == acc)
+        val erased = erase(x)
+        if(acc.contains(erased))
+          distinctBy4(xs, acc)
+        else{
+          val addToAcc =  breakIntoTerms(erased).filter(r => !acc.contains(oneSimp(r)))
+          //val xp = pruneRexp(x, addToAcc)
+          pruneRexp(x, addToAcc) match {
+            case AZERO => distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
+            case xPrime => xPrime :: distinctBy4(xs, addToAcc.map(oneSimp(_)) ::: acc)
+          }
+        }
+    }
 
-// 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)
-// }
+    // fun pAKC_aux :: "arexp list ⇒ arexp ⇒ rexp ⇒ arexp"
+    //   where
+    // "pAKC_aux rsa r ctx = (if (seqFold (SEQ (erase r) ( ctx) )) ⊆ (seqFold (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 seqFold(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
-  case Nil => acc
-  case r :: rs1 => 
-    // if(acc == ONE) 
-    //   seqFold(r, rs1) 
-    // else
-      seqFold(SEQ(acc, r), rs1)
-}
+    //the "fake" Language interpretation: just concatenates!
+    def seqFold(acc: Rexp, rs: List[Rexp]) : Rexp = rs match {
+      case Nil => acc
+      case r :: rs1 => 
+        // if(acc == ONE) 
+        //   seqFold(r, rs1) 
+        // else
+        seqFold(SEQ(acc, r), rs1)
+    }
 
-def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
-def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r)))
-
-def aprint(a: ARexp) = println(shortRexpOutput(erase(a)))
-def asprint(as: List[ARexp]) = as.foreach(a => println(shortRexpOutput(erase(a))))
+    def rprint(r: Rexp) : Unit = println(shortRexpOutput(r))
+    def rsprint(rs: Iterable[Rexp]) = rs.foreach(r => println(shortRexpOutput(r)))
 
-def pAKC(acc: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
-  // println("pakc")
-  // println(shortRexpOutput(erase(r)))
-  // println("acc")
-  // rsprint(acc)
-  // println("ctx---------")
-  // rsprint(ctx)
-  // println("ctx---------end")
-  // rsprint(breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp))
+    def aprint(a: ARexp) = println(shortRexpOutput(erase(a)))
+    def asprint(as: List[ARexp]) = as.foreach(a => println(shortRexpOutput(erase(a))))
 
-  if (breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
-    AZERO
-  }
-  else{
-    r match {
-      case ASEQ(bs, r1, r2) => 
-      (pAKC(acc, r1, erase(r2) :: ctx)) match{
-        case AZERO => 
-          AZERO
-        case AONE(bs1) => 
-          fuse(bs1, r2)
-        case r1p => 
-          ASEQ(bs, r1p, r2)
+    def pAKC(acc: List[Rexp], r: ARexp, ctx: List[Rexp]) : ARexp = {
+      // println("pakc")
+      // println(shortRexpOutput(erase(r)))
+      // println("acc")
+      // rsprint(acc)
+      // println("ctx---------")
+      // rsprint(ctx)
+      // println("ctx---------end")
+      // rsprint(breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp))
+
+      if (breakIntoTerms(seqFold(erase(r), ctx)).map(oneSimp).forall(acc.contains)) {//acc.flatMap(breakIntoTerms
+        AZERO
       }
-      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 => pAKC(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)
+      else{
+        r match {
+          case ASEQ(bs, r1, r2) => 
+            (pAKC(acc, 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"acc is ")
+                // acc.foreach(r => println(shortRexpOutput(r)))
+                rs0.map(r => pAKC(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
         }
-      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 => 
+    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)
-        case xPrime => 
-          xPrime :: distinctBy5(xs, newTerms.map(oneSimp) ::: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: 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 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 isOne1(r: Rexp) : Boolean = r match {
-  case ONE => true
-  case SEQ(r1, r2) => false//isOne1(r1) && isOne1(r2)
-  case ALTS(r1, r2) => false//(isOne1(r1) || isOne1(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
-  case STAR(r0) => false//atMostEmpty(r0)
-  case CHAR(c) => false
-  case ZERO => false
-
-}
-
-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
-}
-
-def furtherSEQ(r11: Rexp, r2: Rexp) : List[Rexp] = {
-  if(r11 == ONE)
-    turnIntoTerms(r2)
-  else
-    SEQ(r11, r2) :: Nil
-}
-
-def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
-  turnIntoTerms((seqFold(erase(r), ctx)))
-    .toSet
-}
-
-def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
-  turnIntoTerms(seqFold(r, ctx)).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)
-}
-def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 
-  //rs1 \subseteq rs2
-  rs1.forall(rs2.contains)
-
-def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {
-  if (ABIncludedByC(a = r, b = ctx, c = acc, 
-                    f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
-  {
-    AZERO
-  }
-  else{
-    r match {
-      case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
-        case AZERO => 
-          AZERO
-        case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
-          prune6(acc, fuse(bs1, r2), ctx)
-        case r1p => 
-          ASEQ(bs, r1p, r2)
-      }
-      case AALTS(bs, rs0) => 
-        rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
-          case Nil => 
-            AZERO
-          case r :: Nil => 
-            fuse(bs, r) 
-          case rs0p => 
-            AALTS(bs, rs0p)
-        }
-      case r => r
-    }
-  }
-}
-
-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 => 
-    Nil
-  case x :: xs => {
-    val erased = erase(x)
-    if(acc.contains(erased)){
-      distinctBy6(xs, acc)
-    }
-    else{
-      val pruned = prune6(acc, x)
-      val newTerms = turnIntoTerms(erase(pruned))
-      pruned match {
-        case AZERO => 
-          distinctBy6(xs, acc)
-        case xPrime => 
-          xPrime :: distinctBy6(xs, newTerms ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
-      }
-    }
-  }
-}
-
-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)
-  case ZERO => Nil
-  case _ => r::Nil
-}
-
-def flatsIntoTerms(r: Rexp) : List[Rexp] = r match {
-  //case SEQ(r1, r2)  => flatsIntoTerms(r1).map(r11 => SEQ(r11, r2))
-  case ALTS(r1, r2) => flatsIntoTerms(r1) ::: flatsIntoTerms(r2)
-  case ZERO => Nil
-  case _ => r::Nil
-}
 
 
-def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
-  case (ONE, bs) => (Empty, bs)
-  case (CHAR(f), bs) => (Chr(f), bs)
-  case (ALTS(r1, r2), Z::bs1) => {
-      val (v, bs2) = decode_aux(r1, bs1)
-      (Left(v), bs2)
-  }
-  case (ALTS(r1, r2), S::bs1) => {
-      val (v, bs2) = decode_aux(r2, bs1)
-      (Right(v), bs2)
-  }
-  case (SEQ(r1, r2), bs) => {
-    val (v1, bs1) = decode_aux(r1, bs)
-    val (v2, bs2) = decode_aux(r2, bs1)
-    (Sequ(v1, v2), bs2)
-  }
-  case (STAR(r1), S::bs) => {
-    val (v, bs1) = decode_aux(r1, bs)
-    //(v)
-    val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
-    (Stars(v::vs), bs2)
-  }
-  case (STAR(_), Z::bs) => (Stars(Nil), bs)
-  case (RECD(x, r1), bs) => {
-    val (v, bs1) = decode_aux(r1, bs)
-    (Rec(x, v), bs1)
-  }
-  case (NOT(r), bs) => (Nots(r.toString), bs)
-}
+    def isOne1(r: Rexp) : Boolean = r match {
+      case ONE => true
+      case SEQ(r1, r2) => false//isOne1(r1) && isOne1(r2)
+      case ALTS(r1, r2) => false//(isOne1(r1) || isOne1(r2)) && (atMostEmpty(r1) && atMostEmpty(r2))//rs.forall(atMostEmpty) && rs.exists(isOne)
+      case STAR(r0) => false//atMostEmpty(r0)
+      case CHAR(c) => false
+      case ZERO => false
+
+    }
+
+    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
+    }
+
+    def furtherSEQ(r11: Rexp, r2: Rexp) : List[Rexp] = {
+      if(r11 == ONE)
+        turnIntoTerms(r2)
+      else
+        SEQ(r11, r2) :: Nil
+    }
+
+    def attachCtx(r: ARexp, ctx: List[Rexp]) : Set[Rexp] = {
+      turnIntoTerms((seqFold(erase(r), ctx)))
+        .toSet
+    }
+
+    def attachCtxcc(r: Rexp, ctx: List[Rexp]) : Set[Rexp] =
+      turnIntoTerms(seqFold(r, ctx)).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)
+    }
+      def rs1_subseteq_rs2(rs1: Set[Rexp], rs2: Set[Rexp]) : Boolean = 
+        //rs1 \subseteq rs2
+      rs1.forall(rs2.contains)
+
+      def prune6(acc: Set[Rexp], r: ARexp, ctx: List[Rexp] = Nil) : ARexp = {
+        if (ABIncludedByC(a = r, b = ctx, c = acc, 
+          f = attachCtx, subseteqPred = rs1_subseteq_rs2)) 
+          {
+            AZERO
+          }
+          else{
+            r match {
+              case ASEQ(bs, r1, r2) => (prune6(acc, r1, erase(r2) :: ctx)) match{
+                case AZERO => 
+                  AZERO
+                case AONE(bs1) => //when r1 becomes 1, chances to further prune r2
+                  prune6(acc, fuse(bs1, r2), ctx)
+                case r1p => 
+                  ASEQ(bs, r1p, r2)
+              }
+                case AALTS(bs, rs0) => 
+                  rs0.map(r => prune6(acc, r, ctx)).filter(_ != AZERO) match {
+                    case Nil => 
+                      AZERO
+                    case r :: Nil => 
+                      fuse(bs, r) 
+                    case rs0p => 
+                      AALTS(bs, rs0p)
+                  }
+                    case r => r
+            }
+          }
+      }
 
-def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
-  case (v, Nil) => v
-  case _ => throw new Exception("Not decodable")
-}
+      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 => 
+          Nil
+        case x :: xs => {
+          val erased = erase(x)
+          if(acc.contains(erased)){
+            distinctBy6(xs, acc)
+          }
+          else{
+            val pruned = prune6(acc, x)
+            val newTerms = turnIntoTerms(erase(pruned))
+            pruned match {
+              case AZERO => 
+                distinctBy6(xs, acc)
+              case xPrime => 
+                xPrime :: distinctBy6(xs, newTerms ++: acc)//distinctBy5(xs, addToAcc.map(oneSimp(_)) ::: acc)
+            }
+          }
+        }
+      }
+
+      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)
+        case ZERO => Nil
+        case _ => r::Nil
+      }
+
+      def flatsIntoTerms(r: Rexp) : List[Rexp] = r match {
+        //case SEQ(r1, r2)  => flatsIntoTerms(r1).map(r11 => SEQ(r11, r2))
+        case ALTS(r1, r2) => flatsIntoTerms(r1) ::: flatsIntoTerms(r2)
+        case ZERO => Nil
+        case _ => r::Nil
+      }
+
+
+      def decode_aux(r: Rexp, bs: Bits) : (Val, Bits) = (r, bs) match {
+        case (ONE, bs) => (Empty, bs)
+        case (CHAR(f), bs) => (Chr(f), bs)
+        case (ALTS(r1, r2), Z::bs1) => {
+          val (v, bs2) = decode_aux(r1, bs1)
+          (Left(v), bs2)
+        }
+        case (ALTS(r1, r2), S::bs1) => {
+          val (v, bs2) = decode_aux(r2, bs1)
+          (Right(v), bs2)
+        }
+        case (SEQ(r1, r2), bs) => {
+          val (v1, bs1) = decode_aux(r1, bs)
+          val (v2, bs2) = decode_aux(r2, bs1)
+          (Sequ(v1, v2), bs2)
+        }
+        case (STAR(r1), S::bs) => {
+          val (v, bs1) = decode_aux(r1, bs)
+          //(v)
+          val (Stars(vs), bs2) = decode_aux(STAR(r1), bs1)
+          (Stars(v::vs), bs2)
+        }
+        case (STAR(_), Z::bs) => (Stars(Nil), bs)
+        case (RECD(x, r1), bs) => {
+          val (v, bs1) = decode_aux(r1, bs)
+          (Rec(x, v), bs1)
+        }
+        case (NOT(r), bs) => (Nots(r.toString), bs)
+      }
+
+      def decode(r: Rexp, bs: Bits) = decode_aux(r, bs) match {
+        case (v, Nil) => v
+        case _ => throw new Exception("Not decodable")
+      }
 
 
 
-def blexing_simp(r: Rexp, s: String) : Val = {
-    val bit_code = blex_simp(internalise(r), s.toList)
-    decode(r, bit_code)
-}
-def simpBlexer(r: Rexp, s: String) : Val = {
-  Try(blexing_simp(r, s)).getOrElse(Failure)
-}
-
-def strong_blexing_simp(r: Rexp, s: String) : Val = {
-  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)) {
-      //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 = strongBsimp(der_res)  
-    strong_blex_simp(simp_res, cs)      
-  }
-}
-
-def strong_blex_simp5(r: ARexp, s: List[Char]) : Bits = s match {
-  case Nil => {
-    if (bnullable(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 blexing_simp(r: Rexp, s: String) : Val = {
+        val bit_code = blex_simp(internalise(r), s.toList)
+        decode(r, bit_code)
+      }
+      def simpBlexer(r: Rexp, s: String) : Val = {
+        Try(blexing_simp(r, s)).getOrElse(Failure)
+      }
 
-  def bders_simp(s: List[Char], r: ARexp) : ARexp = s match {
-    case Nil => r
-    case c::s => 
-      //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 bdersStrong6(s: List[Char], r: ARexp) : ARexp = s match {
-    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 {
-    case Nil => r 
-    case c::s => bdersStrong(s, strongBsimp(bder(c, r)))
-  }
-
-  def bdersStrongRexp(s: String, r: Rexp) : ARexp = bdersStrong(s.toList, internalise(r))
-
-  def erase(r:ARexp): Rexp = r match{
-    case AZERO => ZERO
-    case AONE(_) => ONE
-    case ACHAR(bs, c) => CHAR(c)
-    case AALTS(bs, Nil) => ZERO
-    case AALTS(bs, a::Nil) => erase(a)
-    case AALTS(bs, a::as) => ALTS(erase(a), erase(AALTS(bs, as)))
-    case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
-    case ASTAR(cs, r)=> STAR(erase(r))
-    case ANOT(bs, r) => NOT(erase(r))
-    case AANYCHAR(bs) => ANYCHAR
-  }
+      def strong_blexing_simp(r: Rexp, s: String) : Val = {
+        decode(r, strong_blex_simp(internalise(r), s.toList))
+      }
 
-
-  def allCharSeq(r: Rexp) : Boolean = r match {
-    case CHAR(c) => true
-    case SEQ(r1, r2) => allCharSeq(r1) && allCharSeq(r2)
-    case _ => false
-  }
-
-  def flattenSeq(r: Rexp) : String = r match {
-    case CHAR(c) => c.toString
-    case SEQ(r1, r2) => flattenSeq(r1) ++ flattenSeq(r2)
-    case _ => throw new Error("flatten unflattenable rexp")
-  } 
-
-  def shortRexpOutput(r: Rexp) : String = r match {
-      case CHAR(c) => c.toString
-      case ONE => "1"
-      case ZERO => "0"
-      case SEQ(r1, r2) if(allCharSeq(r)) => flattenSeq(r)//"[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
-      case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
-      case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
-      case STAR(STAR(r)) => "(..)*"// ++ shortRexpOutput(r) ++ "]*"
-      case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
-      //case RTOP => "RTOP"
-    }
-
-
-  def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
-      case Nil => {
-        if (bnullable(r)) {
-          val bits = mkepsBC(r)
-          bits
-        }
-        else 
-          throw new Exception("Not matched")
+      def strong_blexing_simp5(r: Rexp, s: String) : Val = {
+        decode(r, strong_blex_simp5(internalise(r), s.toList))
       }
-      case c::cs => {
-        val der_res = bder(c,r)
-        val simp_res = bsimp(der_res)  
-        blex_simp(simp_res, cs)      
-      }
-  }
 
 
 
 
-    def size(r: Rexp) : Int = r match {
-      case ZERO => 1
-      case ONE => 1
-      case CHAR(_) => 1
-      case ANYCHAR => 1
-      case NOT(r0) => 1 + size(r0)
-      case SEQ(r1, r2) => 1 + size(r1) + size(r2)
-      case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
-      case STAR(r) => 1 + size(r)
+      //def blexerStrong(r: ARexp, 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 strongBlexer(r: Rexp, s: String) : Option[Val] = {
+        Try(Some(decode(r, strong_blex_simp(internalise(r), s.toList)))).getOrElse(None)
+      }
+      def strong_blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
+        case Nil => {
+          if (bnullable(r)) {
+            mkepsBC(r)
+          }
+          else 
+            throw new Exception("Not matched")
+        }
+        case c::cs => {
+          strong_blex_simp(strongBsimp(bder(c, r)), cs)      
+        }
+      }
+
+      def strong_blex_simp5(r: ARexp, s: List[Char]) : Bits = s match {
+        case Nil => {
+          if (bnullable(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))
+          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 bdersStrong6(s: List[Char], r: ARexp) : ARexp = s match {
+        case Nil => r
+        case c::s => bdersStrong6(s, strongBsimp6(bder(c, r)))
+      }
+      //Conjecture: [| bdersStrong(s, r) |] = O([| r |]^3)
+      def bdersStrong(s: List[Char], r: ARexp) : ARexp = s match {
+        case Nil => r
+        case c::s => bdersStrong(s, bsimpStrong(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 {
+      //  case Nil => r 
+      //  case c::s => bdersStrong(s, strongBsimp(bder(c, r)))
+      //}
+
+      def bdersStrongRexp(s: String, r: Rexp) : ARexp = bdersStrong(s.toList, internalise(r))
+
+      def erase(r:ARexp): Rexp = r match{
+        case AZERO => ZERO
+        case AONE(_) => ONE
+        case ACHAR(bs, c) => CHAR(c)
+        case AALTS(bs, Nil) => ZERO
+        case AALTS(bs, a::Nil) => erase(a)
+        case AALTS(bs, a::as) => ALTS(erase(a), erase(AALTS(bs, as)))
+        case ASEQ(bs, r1, r2) => SEQ (erase(r1), erase(r2))
+        case ASTAR(cs, r)=> STAR(erase(r))
+        case ANOT(bs, r) => NOT(erase(r))
+        case AANYCHAR(bs) => ANYCHAR
+      }
+
+
+      def allCharSeq(r: Rexp) : Boolean = r match {
+        case CHAR(c) => true
+        case SEQ(r1, r2) => allCharSeq(r1) && allCharSeq(r2)
+        case _ => false
+      }
+
+      def flattenSeq(r: Rexp) : String = r match {
+        case CHAR(c) => c.toString
+        case SEQ(r1, r2) => flattenSeq(r1) ++ flattenSeq(r2)
+        case _ => throw new Error("flatten unflattenable rexp")
+      } 
+
+      def shortRexpOutput(r: Rexp) : String = r match {
+        case CHAR(c) => c.toString
+        case ONE => "1"
+        case ZERO => "0"
+        case SEQ(r1, r2) if(allCharSeq(r)) => flattenSeq(r)//"[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
+        case SEQ(r1, r2) => "[" ++ shortRexpOutput(r1) ++ "~" ++ shortRexpOutput(r2) ++ "]"
+        case ALTS(r1, r2) => "(" ++ shortRexpOutput(r1) ++ "+" ++ shortRexpOutput(r2) ++ ")"
+        case STAR(STAR(r)) => "(..)*"// ++ shortRexpOutput(r) ++ "]*"
+        case STAR(r) => "STAR(" ++ shortRexpOutput(r) ++ ")"
+        //case RTOP => "RTOP"
+      }
+
+
+      def blex_simp(r: ARexp, s: List[Char]) : Bits = s match {
+        case Nil => {
+          if (bnullable(r)) {
+            val bits = mkepsBC(r)
+            bits
+          }
+          else 
+            throw new Exception("Not matched")
+        }
+        case c::cs => {
+          val der_res = bder(c,r)
+          val simp_res = bsimp(der_res)  
+          blex_simp(simp_res, cs)      
+        }
+      }
+
+
+
+
+      def size(r: Rexp) : Int = r match {
+        case ZERO => 1
+        case ONE => 1
+        case CHAR(_) => 1
+        case ANYCHAR => 1
+        case NOT(r0) => 1 + size(r0)
+        case SEQ(r1, r2) => 1 + size(r1) + size(r2)
+        case ALTS(r1, r2) => 1 + List(r1, r2).map(size).sum
+        case STAR(r) => 1 + size(r)
+      }
+
+      def asize(a: ARexp) = size(erase(a))
+
+      //pder related
+      type Mon = (Char, Rexp)
+      type Lin = Set[Mon]
+
+      def dot_prod(rs: Set[Rexp], r: Rexp): Set[Rexp] = r match {
+        case ZERO => Set()
+        case ONE => rs
+        case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
+      }
+      def cir_prod(l: Lin, t: Rexp): Lin = t match {//remember this Lin is different from the Lin in Antimirov's paper. Here it does not mean the set of all subsets of linear forms that does not contain zero, but rather the type a set of linear forms
+        case ZERO => Set()
+        // case ONE => l
+        case t => l.map( m => m._2 match 
+        {
+          case ZERO => m 
+          case ONE => (m._1, t) 
+          case p => (m._1, SEQ(p, t)) 
+        }  
+
+        )
+      }
+      def cir_prodList(l : List[Mon], t: Rexp): List[Mon] = t match {
+        case ZERO => Nil
+        case ONE => l
+        case t => l.map(m => m._2 match
+        {
+          case ZERO => m
+          case ONE => (m._1, t)
+          case p => (m._1, SEQ(p, t))
+        }
+        )
+
+      }
+      def lfList(r: Rexp) : List[Mon] = r match {
+        case ZERO => Nil
+        case ONE => Nil
+        case CHAR(f) => {
+          (f, ONE) :: Nil
+        }
+        case ALTS(r1, r2) => {
+          lfList(r1) ++ lfList(r2)
+        }
+        case STAR(r1) => cir_prodList(lfList(r1), STAR(r1))
+        case SEQ(r1, r2) => {
+          if(nullable(r1))
+            cir_prodList(lfList(r1), r2) ++ lfList(r2)
+          else
+            cir_prodList(lfList(r1), r2)
+        }
+      }
+      def lfprint(ls: Lin) = ls.foreach(m =>{
+        println(m._1)
+        rprint(m._2)
+      })
+    def lf(r: Rexp): Lin = r match {
+      case ZERO => Set()
+      case ONE => Set()
+      case CHAR(f) => {
+        //val Some(c) = alphabet.find(f) 
+        Set((f, ONE))
+      }
+      case ALTS(r1, r2) => {
+        lf(r1 ) ++ lf(r2)
+      }
+      case STAR(r1) => cir_prod(lf(r1), STAR(r1)) //may try infix notation later......
+      case SEQ(r1, r2) =>{
+        if (nullable(r1))
+          cir_prod(lf(r1), r2) ++ lf(r2)
+        else
+          cir_prod(lf(r1), r2) 
+      }
+    }
+    def lfs(r: Set[Rexp]): Lin = {
+      r.foldLeft(Set[Mon]())((acc, r) => acc ++ lf(r))
     }
 
-    def asize(a: ARexp) = size(erase(a))
-
-//pder related
-type Mon = (Char, Rexp)
-type Lin = Set[Mon]
-
-def dot_prod(rs: Set[Rexp], r: Rexp): Set[Rexp] = r match {
-    case ZERO => Set()
-    case ONE => rs
-    case r => rs.map((re) => if (re == ONE) r else SEQ(re, r)  )   
-  }
-  def cir_prod(l: Lin, t: Rexp): Lin = t match {//remember this Lin is different from the Lin in Antimirov's paper. Here it does not mean the set of all subsets of linear forms that does not contain zero, but rather the type a set of linear forms
-    case ZERO => Set()
-    // case ONE => l
-    case t => l.map( m => m._2 match 
-      {
-        case ZERO => m 
-        case ONE => (m._1, t) 
-        case p => (m._1, SEQ(p, t)) 
-      }  
-    
-    )
-  }
-  def cir_prodList(l : List[Mon], t: Rexp): List[Mon] = t match {
-    case ZERO => Nil
-    case ONE => l
-    case t => l.map(m => m._2 match
-      {
-        case ZERO => m
-        case ONE => (m._1, t)
-        case p => (m._1, SEQ(p, t))
-      }
-    )
-
-  }
-  def lfList(r: Rexp) : List[Mon] = r match {
-    case ZERO => Nil
-    case ONE => Nil
-    case CHAR(f) => {
-      (f, ONE) :: Nil
+    def pder(x: Char, t: Rexp): Set[Rexp] = {
+      val lft = lf(t)
+      (lft.filter(mon => if(mon._1 == x) true else false)).map(mon => mon._2)
     }
-    case ALTS(r1, r2) => {
-      lfList(r1) ++ lfList(r2)
+    def pders_single(s: List[Char], t: Rexp) : Set[Rexp] = s match {
+      case x::xs => pders(xs, pder(x, t))
+      case Nil => Set(t)
     }
-    case STAR(r1) => cir_prodList(lfList(r1), STAR(r1))
-    case SEQ(r1, r2) => {
-      if(nullable(r1))
-        cir_prodList(lfList(r1), r2) ++ lfList(r2)
-      else
-        cir_prodList(lfList(r1), r2)
+    def pders(s: List[Char], ts: Set[Rexp]) : Set[Rexp] = s match {
+      case x::xs => pders(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
+      case Nil => ts 
     }
-  }
-  def lfprint(ls: Lin) = ls.foreach(m =>{
-    println(m._1)
-    rprint(m._2)
-    })
-  def lf(r: Rexp): Lin = r match {
-    case ZERO => Set()
-    case ONE => Set()
-    case CHAR(f) => {
-      //val Some(c) = alphabet.find(f) 
-      Set((f, ONE))
-    }
-    case ALTS(r1, r2) => {
-      lf(r1 ) ++ lf(r2)
-    }
-    case STAR(r1) => cir_prod(lf(r1), STAR(r1)) //may try infix notation later......
-    case SEQ(r1, r2) =>{
-      if (nullable(r1))
-        cir_prod(lf(r1), r2) ++ lf(r2)
-      else
-        cir_prod(lf(r1), r2) 
-    }
-  }
-  def lfs(r: Set[Rexp]): Lin = {
-    r.foldLeft(Set[Mon]())((acc, r) => acc ++ lf(r))
-  }
-
-  def pder(x: Char, t: Rexp): Set[Rexp] = {
-    val lft = lf(t)
-    (lft.filter(mon => if(mon._1 == x) true else false)).map(mon => mon._2)
-  }
-  def pders_single(s: List[Char], t: Rexp) : Set[Rexp] = s match {
-    case x::xs => pders(xs, pder(x, t))
-    case Nil => Set(t)
-  }
-  def pders(s: List[Char], ts: Set[Rexp]) : Set[Rexp] = s match {
-    case x::xs => pders(xs, ts.foldLeft(Set[Rexp]())((acc, t) => acc ++ pder(x, t)))
-    case Nil => ts 
-  }
-  def pderss(ss: List[List[Char]], t: Rexp): Set[Rexp] = 
-    ss.foldLeft( Set[Rexp]() )( (acc, s) => pders_single(s, t) ++ acc )
-  def pdera(t: Rexp): Set[Rexp] = lf(t).map(mon => mon._2)
-  //all implementation of partial derivatives that involve set union are potentially buggy
-  //because they don't include the original regular term before they are pdered.
-  //now only pderas is fixed.
-  def pderas(t: Set[Rexp], d: Int): Set[Rexp] = 
-    if(d > 0) 
-      pderas(lfs(t).map(mon => mon._2), d - 1) ++ t 
-    else 
-      lfs(t).map(mon => mon._2) ++ t//repeated application of pderas over the newest set of pders.
+    def pderss(ss: List[List[Char]], t: Rexp): Set[Rexp] = 
+      ss.foldLeft( Set[Rexp]() )( (acc, s) => pders_single(s, t) ++ acc )
+    def pdera(t: Rexp): Set[Rexp] = lf(t).map(mon => mon._2)
+    //all implementation of partial derivatives that involve set union are potentially buggy
+    //because they don't include the original regular term before they are pdered.
+    //now only pderas is fixed.
+    def pderas(t: Set[Rexp], d: Int): Set[Rexp] = 
+      if(d > 0) 
+        pderas(lfs(t).map(mon => mon._2), d - 1) ++ t 
+      else 
+        lfs(t).map(mon => mon._2) ++ t//repeated application of pderas over the newest set of pders.
   def pderUNIV(r: Rexp) : Set[Rexp] = pderas(Set(r), awidth(r) + 1)
   def awidth(r: Rexp) : Int = r match {
     case CHAR(c) => 1
@@ -1384,275 +1385,275 @@
 
 
 
-def starPrint(r: Rexp) : Unit = r match {
-        
-          case SEQ(head, rstar) =>
-            println(shortRexpOutput(head) ++ "~STARREG")
-          case STAR(rstar) =>
-            println("STARREG")
-          case ALTS(r1, r2) =>  
-            println("(")
-            starPrint(r1)
-            println("+")
-            starPrint(r2)
-            println(")")
-          case ZERO => println("0")
+  def starPrint(r: Rexp) : Unit = r match {
+
+    case SEQ(head, rstar) =>
+      println(shortRexpOutput(head) ++ "~STARREG")
+    case STAR(rstar) =>
+      println("STARREG")
+    case ALTS(r1, r2) =>  
+      println("(")
+      starPrint(r1)
+      println("+")
+      starPrint(r2)
+      println(")")
+    case ZERO => println("0")
+  }
+
+  // @arg(doc = "small tests")
+  def n_astar_list(d: Int) : Rexp = {
+    if(d == 0) STAR("a") 
+    else ALTS(STAR("a" * d), n_astar_list(d - 1))
+  }
+  def n_astar_alts(d: Int) : Rexp = d match {
+    case 0 => n_astar_list(0)
+    case d => STAR(n_astar_list(d))
+  }
+  def n_astar_alts2(d: Int) : Rexp = d match {
+    case 0 => n_astar_list(0)
+    case d => STAR(STAR(n_astar_list(d)))
+  }
+  def n_astar_aux(d: Int) = {
+    if(d == 0) n_astar_alts(0)
+    else ALTS(n_astar_alts(d), n_astar_alts(d - 1))
+  }
+
+  def n_astar(d: Int) : Rexp = STAR(n_astar_aux(d))
+  //val STARREG = n_astar(3)
+  // ( STAR("a") | 
+  //                  ("a" | "aa").% | 
+  //                 ( "a" | "aa" | "aaa").% 
+  //                 ).%
+  //( "a" | "aa" | "aaa" | "aaaa").% |
+  //( "a" | "aa" | "aaa" | "aaaa" | "aaaaa").% 
+  (((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).%
+
+  // @main
+
+  def lcm(list: Seq[Int]):Int=list.foldLeft(1:Int){
+    (a, b) => b * a /
+    Stream.iterate((a,b)){case (x,y) => (y, x%y)}.dropWhile(_._2 != 0).head._1.abs
+  }
+
+  def small() = {
+    //val pderSTAR = pderUNIV(STARREG)
+
+    //val refSize = pderSTAR.map(size(_)).sum
+    for(n <- 5 to 5){
+      val STARREG = n_astar_alts2(n)
+      val iMax = (lcm((1 to n).toList))
+      for(i <- 0 to iMax ){// 100, 400, 800, 840, 841, 900 
+        val prog0 = "a" * i
+        //println(s"test: $prog0")
+        print(i)
+        print(" ")
+        // print(i)
+        // print(" ")
+        println(asize(bders_simp(prog0.toList, internalise(STARREG))))
+        // println(asize(bdersStrong(prog0.toList, internalise(STARREG))))
       }
 
-// @arg(doc = "small tests")
-def n_astar_list(d: Int) : Rexp = {
-  if(d == 0) STAR("a") 
-  else ALTS(STAR("a" * d), n_astar_list(d - 1))
-}
-def n_astar_alts(d: Int) : Rexp = d match {
-  case 0 => n_astar_list(0)
-  case d => STAR(n_astar_list(d))
-  }
-def n_astar_alts2(d: Int) : Rexp = d match {
-  case 0 => n_astar_list(0)
-  case d => STAR(STAR(n_astar_list(d)))
+    }
   }
-def n_astar_aux(d: Int) = {
-  if(d == 0) n_astar_alts(0)
-  else ALTS(n_astar_alts(d), n_astar_alts(d - 1))
-}
-
-def n_astar(d: Int) : Rexp = STAR(n_astar_aux(d))
-//val STARREG = n_astar(3)
-// ( STAR("a") | 
-//                  ("a" | "aa").% | 
-//                 ( "a" | "aa" | "aaa").% 
-//                 ).%
-                //( "a" | "aa" | "aaa" | "aaaa").% |
-                //( "a" | "aa" | "aaa" | "aaaa" | "aaaaa").% 
-(((STAR("a") | ( STAR("aaa")) | STAR("aaaaa"| ( STAR("aaaaaaa")) | STAR("aaaaaaaaaaa"))).%).%).%
-
-// @main
-
-def lcm(list: Seq[Int]):Int=list.foldLeft(1:Int){
-  (a, b) => b * a /
-  Stream.iterate((a,b)){case (x,y) => (y, x%y)}.dropWhile(_._2 != 0).head._1.abs
-}
+  // small()
 
-def small() = {
-  //val pderSTAR = pderUNIV(STARREG)
-
-  //val refSize = pderSTAR.map(size(_)).sum
-  for(n <- 5 to 5){
-    val STARREG = n_astar_alts2(n)
-    val iMax = (lcm((1 to n).toList))
-    for(i <- 0 to iMax ){// 100, 400, 800, 840, 841, 900 
-      val prog0 = "a" * i
-      //println(s"test: $prog0")
-      print(i)
-      print(" ")
-      // print(i)
-      // print(" ")
-      println(asize(bders_simp(prog0.toList, internalise(STARREG))))
-      // println(asize(bdersStrong7(prog0.toList, internalise(STARREG))))
+  def aaa_star() = {
+    val r = STAR(("a" | "aa"))
+    for(i <- 0 to 20) {
+      val prog = "a" * i
+      print(i+" ")
+      println(asize(bders_simp(prog.toList, internalise(r))))
+      //println(size(ders_simp(prog.toList, r)))
     }
-    
   }
-}
-// small()
+  // aaa_star()
 
-def aaa_star() = {
-  val r = STAR(("a" | "aa"))
-  for(i <- 0 to 20) {
-    val prog = "a" * i
-    print(i+" ")
-    println(asize(bders_simp(prog.toList, internalise(r))))
-    //println(size(ders_simp(prog.toList, r)))
-  }
-}
-// aaa_star()
-
-def matching_ways_counting(n: Int): Int = 
+  def matching_ways_counting(n: Int): Int = 
   {
     if(n == 0) 1
     else if(n == 1) 2
     else (for(i <- 1 to n - 1) 
       yield matching_ways_counting(i) * matching_ways_counting(n - i) ).sum + (n + 1)
   }
-def naive_matcher() {
-  val r = STAR(STAR("a") ~ STAR("a"))
+  def naive_matcher() {
+    val r = STAR(STAR("a") ~ STAR("a"))
 
-  // for(i <- 0 to 10) {
-  //   val s = "a" * i 
-  //   val t1 = System.nanoTime
-  //   matcher(s, r)
-  //   val duration = (System.nanoTime - t1) / 1e9d
-  //   print(i)
-  //   print(" ")
-  //   // print(duration)
-  //   // print(" ")
-  //   (aprint(bders_simp(s.toList, internalise(r))))
-  //   //print(size(ders_simp(s.toList, r)))
-  //   println()
-  // }
-  for(i <- 1 to 3) {
-    val s = "a" * i
-    val t1 = System.nanoTime
-    val derssimp_result = ders_simp(s.toList, r)
-    println(i)
-    println(matching_ways_counting(i))
-    println(size(derssimp_result))
-    rprint(derssimp_result)
+    // for(i <- 0 to 10) {
+    //   val s = "a" * i 
+    //   val t1 = System.nanoTime
+    //   matcher(s, r)
+    //   val duration = (System.nanoTime - t1) / 1e9d
+    //   print(i)
+    //   print(" ")
+    //   // print(duration)
+    //   // print(" ")
+    //   (aprint(bders_simp(s.toList, internalise(r))))
+    //   //print(size(ders_simp(s.toList, r)))
+    //   println()
+    // }
+    for(i <- 1 to 3) {
+      val s = "a" * i
+      val t1 = System.nanoTime
+      val derssimp_result = ders_simp(s.toList, r)
+      println(i)
+      println(matching_ways_counting(i))
+      println(size(derssimp_result))
+      rprint(derssimp_result)
+    }
+
   }
-  
-}
-naive_matcher()
-//single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
-//  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE)))
+  naive_matcher()
+  //single(SEQ(SEQ(STAR(CHAR('b')),STAR(STAR(SEQ(CHAR('a'),CHAR('b'))))),
+  //  SEQ(SEQ(CHAR('b'),STAR(ALTS(CHAR('a'),ONE))),ONE)))
 
 
-//STAR(SEQ(ALTS(CHAR(b),STAR(CHAR(b))),ALTS(ALTS(ONE,CHAR(b)),SEQ(CHAR(c),ONE))))
-def generator_test() {
+  //STAR(SEQ(ALTS(CHAR(b),STAR(CHAR(b))),ALTS(ALTS(ONE,CHAR(b)),SEQ(CHAR(c),ONE))))
+  def generator_test() {
 
-  test(single(STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))), 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("ab")//stringsFromRexp(r)
-    val boolList = ss.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 => turnIntoTerms(r))
-      val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
-      (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
-      
-    })
-    //!boolList.exists(b => b == false)
-    !boolList.exists(b => b == false)
-  }
-}
-// small()
-// generator_test()
+    test(single(STAR(SEQ(ALTS(STAR(CHAR('b')),ALTS(CHAR('b'),CHAR('a'))),ALTS(ALTS(CHAR('b'),CHAR('c')),STAR(ZERO))))), 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("ab")//stringsFromRexp(r)
+      val boolList = ss.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 => turnIntoTerms(r))
+        val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
+        (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
+
+      })
+      //!boolList.exists(b => b == false)
+      !boolList.exists(b => b == false)
+      }
+    }
+    // small()
+    // 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))))
+    //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))))
 
-//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)))))
-//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'))),
-    //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))
-  // 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)
+    //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)))))
+    //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'))),
+      //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))
+      // 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 lf_display() {
-  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'))),
-    //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)
-  lfprint(lf(r))
+    def lf_display() {
+      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'))),
+      //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)
+      lfprint(lf(r))
 
-}
+    }
 
-lf_display()
+    lf_display()
 
-def breakable(r: Rexp) : Boolean = r match {
-  case SEQ(ALTS(_, _), _) => true
-  case SEQ(r1, r2) => breakable(r1)
-  case _ => false
-}
+    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))) //
-  val r_linforms = lf(r)
-  println(r_linforms.size)
-  val pderuniv = pderUNIV(r)
-  println(pderuniv.size)
-}
-// linform_test()
-// 1
-def newStrong_test() {
-  val r2 = (CHAR('b') | ONE)
-  val r0 = CHAR('d')
-  val r1 = (ONE | CHAR('c'))
-  val expRexp = (SEQ(r2, r0) | SEQ(SEQ(r1, r2), r0))
-  println(s"original regex is: ")
-  rprint(expRexp)
-  val expSimp5 = strongBsimp5(internalise(expRexp))
-  val expSimp6 = strongBsimp6(internalise(expRexp))
-  aprint(expSimp5)
-  aprint(expSimp6)
-}
-// newStrong_test()
-// 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))
+    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)
+      println(r_linforms.size)
+      val pderuniv = pderUNIV(r)
+      println(pderuniv.size)
+    }
+    // linform_test()
+    // 1
+    def newStrong_test() {
+      val r2 = (CHAR('b') | ONE)
+      val r0 = CHAR('d')
+      val r1 = (ONE | CHAR('c'))
+      val expRexp = (SEQ(r2, r0) | SEQ(SEQ(r1, r2), r0))
+      println(s"original regex is: ")
+      rprint(expRexp)
+      val expSimp5 = strongBsimp5(internalise(expRexp))
+      val expSimp6 = strongBsimp6(internalise(expRexp))
+      aprint(expSimp5)
+      aprint(expSimp6)
+    }
+    // newStrong_test()
+    // 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))
 
 
-// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
-// Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
+    // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
+    // Sequ(Sequ(Sequ(Empty,Chr(b)),Stars(List(Chr(b), Chr(b)))),Sequ(Right(Stars(List(Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty)), Right(Sequ(Sequ(Stars(List(Right(Chr(a)), Right(Chr(a)))),Sequ(Chr(a),Sequ(Left(Chr(b)),Sequ(Empty,Chr(b))))),Empty))))),Empty))
 
 
 
 
 
-def bders_bderssimp() {
+    def bders_bderssimp() {
 
-  test(single(SEQ(ALTS(ONE,CHAR('c')),
-  SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))))), 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("aa")//stringsFromRexp(r)
-    val boolList = ss.map(s => {
-      //val bdStrong = bdersStrong(s.toList, internalise(r))
-      val bds = bsimp(bders(s.toList, internalise(r)))
-      val bdssimp = bsimp(bders_simp(s.toList, internalise(r)))
-      //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
-      //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
-      //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
-      rprint(r)
-      println(bds)
-      println(bdssimp)
-      bds == bdssimp
-    })
-    //!boolList.exists(b => b == false)
-    !boolList.exists(b => b == false)
-  }
-}
-//  bders_bderssimp()
-  
+      test(single(SEQ(ALTS(ONE,CHAR('c')),
+        SEQ(SEQ(CHAR('a'),CHAR('a')),ALTS(ONE,CHAR('c'))))), 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("aa")//stringsFromRexp(r)
+          val boolList = ss.map(s => {
+            //val bdStrong = bdersStrong(s.toList, internalise(r))
+            val bds = bsimp(bders(s.toList, internalise(r)))
+            val bdssimp = bsimp(bders_simp(s.toList, internalise(r)))
+            //val pdersSet = pderUNIV(r)//.flatMap(r => turnIntoTerms(r))
+            //val pdersSetBroken = pdersSet.flatMap(r => turnIntoTerms(r))
+            //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
+            rprint(r)
+            println(bds)
+            println(bdssimp)
+            bds == bdssimp
+          })
+          //!boolList.exists(b => b == false)
+          !boolList.exists(b => b == false)
+          }
+        }
+        //  bders_bderssimp()
 
 
+

--- a/thys4/posix/FBound.thy	Wed Aug 31 23:57:42 2022 +0100
+++ b/thys4/posix/FBound.thy	Thu Sep 01 23:47:37 2022 +0100
@@ -279,13 +279,16 @@
   using leq1.intros(1) leq1.intros(16) by force
 
 lemma dB_leq12:
-  shows "AALTs bs (distinctWith rs1 eq1 (set rs2)) \<le>1 AALTs bs (rs1 @ rs2)"
+  shows "AALTs bs (rs1 @ (distinctWith rs1 eq1 (set rs2))) \<le>1 AALTs bs (rs1 @ rs2)"
+  apply(induct rs1 arbitrary: rs2)
+  apply simp
   sorry
 
 
 lemma dB_leq1:
   shows "AALTs bs (distinctWith rs eq1 {}) \<le>1 AALTs bs rs"
-  by (metis append.right_neutral dB_leq12 list.set(1))
+  sorry
+