1894 \section{A Bound for the Star Regular Expression}

  1895 We have shown how to control the size of the sequence regular expression $r_1\cdot r_2$ using

  1896 the "closed form" of $(r_1 \cdot r_2) \backslash s$ and then 

  1897 the property of the $\distinct$ function.

  1898 Now we try to get a bound on $r^* \backslash s$ as well.

  1899 Again, we first look at how a star's derivatives evolve, if they grow maximally: 

  1900 \begin{center}

  1901 

  1902 $r^* \quad \longrightarrow_{\backslash c}  \quad   (r\backslash c)  \cdot  r^* \quad \longrightarrow_{\backslash c'}  \quad

  1903 r \backslash cc'  \cdot r^* + r \backslash c' \cdot r^*  \quad \longrightarrow_{\backslash c''} \quad 

  1904 (r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') + (r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*)   \quad \longrightarrow_{\backslash c'''}

  1905 \quad \ldots$

  1906 

  1907 \end{center}

  1908 When we have a string $s = c :: c' :: c'' \ldots$  such that $r \backslash c$, $r \backslash cc'$, $r \backslash c'$, 

  1909 $r \backslash cc'c''$, $r \backslash c'c''$, $r\backslash c''$ etc. are all nullable,

  1910 the number of terms in $r^* \backslash s$ will grow exponentially, causing the size

  1911 of the derivatives $r^* \backslash s$ to grow exponentially, even if we do not 

  1912 count the possible size explosions of $r \backslash c$ themselves.

  1913 

  1914 Thanks to $\flts$ and $\distinctWith$, we are able to open up regexes like

  1915 $(r_1 \backslash cc'c'' \cdot r^* + r \backslash c'') + (r \backslash c'c'' \cdot r^* + r \backslash c'' \cdot r^*) $ 

  1916 into $\RALTS{[r_1 \backslash cc'c'' \cdot r^*, r \backslash c'', r \backslash c'c'' \cdot r^*, r \backslash c'' \cdot r^*]}$

  1917 and then de-duplicate terms of the form $r\backslash s' \cdot r^*$ ($s'$ being a substring of $s$).

  1918 For this we define $\hflataux{\_}$ and $\hflat{\_}$, similar to $\sflataux{\_}$ and $\sflat{\_}$:

  1919 %TODO: definitions of  and \hflataux \hflat

  1920  \begin{center}  

  1921  \begin{tabular}{ccc}

  1922  $\hflataux{r_1 + r_2}$ & $=$ & $\hflataux{r_1} @ \hflataux{r_2}$\\

  1923 $\hflataux r$ & $=$ & $ [r]$

  1924 \end{tabular}

  1925 \end{center}

  1926 

  1927  \begin{center}  

  1928  \begin{tabular}{ccc}

  1929  $\hflat{r_1 + r_2}$ & $=$ & $\RALTS{\hflataux{r_1} @ \hflataux{r_2}}$\\

  1930 $\hflat r$ & $=$ & $ r$

  1931 \end{tabular}

  1932 \end{center}s

  1933 Again these definitions are tailor-made for dealing with alternatives that have

  1934 originated from a star's derivatives, so we don't attempt to open up all possible 

  1935 regexes of the form $\RALTS{rs}$, where $\textit{rs}$ might not contain precisely 2

  1936 elements.

  1937 We give a predicate for such "star-created" regular expressions:

  1938 \begin{center}

  1939 \begin{tabular}{lcr}

  1940          &    &       $\createdByStar{(\RSEQ{ra}{\RSTAR{rb}}) }$\\

  1941  $\createdByStar{r_1} \land \createdByStar{r_2} $ & $ \Longrightarrow$ & $\createdByStar{(r_1 + r_2)}$

  1942  \end{tabular}

  1943  \end{center}

  1944  

  1945  These definitions allows us the flexibility to talk about 

  1946  regular expressions in their most convenient format,

  1947  for example, flattened out $\RALTS{[r_1, r_2, \ldots, r_n]} $

  1948  instead of binary-nested: $((r_1 + r_2) + (r_3 + r_4)) + \ldots$.

  1949  These definitions help express that certain classes of syntatically 

  1950  distinct regular expressions are actually the same under simplification.

  1951  This is not entirely true for annotated regular expressions: 

  1952  %TODO: bsimp bders \neq bderssimp

  1953  \begin{center}

  1954  $(1+ (c\cdot \ASEQ{bs}{c^*}{c} ))$

  1955  \end{center}

  1956  For bit-codes, the order in which simplification is applied

  1957  might cause a difference in the location they are placed.

  1958  If we want something like

  1959  \begin{center}

  1960  $\bderssimp{r}{s} \myequiv \bsimp{\bders{r}{s}}$

  1961  \end{center}

  1962  Some "canonicalization" procedure is required,

  1963  which either pushes all the common bitcodes to nodes

  1964   as senior as possible:

  1965   \begin{center}

  1966   $_{bs}(_{bs_1 @ bs'}r_1 + _{bs_1 @ bs''}r_2) \rightarrow _{bs @ bs_1}(_{bs'}r_1 + _{bs''}r_2) $

  1967   \end{center}

  1968  or does the reverse. However bitcodes are not of interest if we are talking about

  1969  the $\llbracket r \rrbracket$ size of a regex.

  1970  Therefore for the ease and simplicity of producing a

  1971  proof for a size bound, we are happy to restrict ourselves to 

  1972  unannotated regular expressions, and obtain such equalities as

  1973  \begin{lemma}

  1974  $\rsimp{r_1 + r_2} = \rsimp{\RALTS{\hflataux{r_1} @ \hflataux{r_2}}}$

  1975  \end{lemma}

  1976  

  1977  \begin{proof}

  1978  By using the rewriting relation $\rightsquigarrow$

  1979  \end{proof}

  1980  %TODO: rsimp sflat

  1981 And from this we obtain a proof that a star's derivative will be the same

  1982 as if it had all its nested alternatives created during deriving being flattened out:

  1983  For example,

  1984  \begin{lemma}

  1985  $\createdByStar{r} \implies \rsimp{r} = \rsimp{\RALTS{\hflataux{r}}}$

  1986  \end{lemma}

  1987  \begin{proof}

  1988  By structural induction on $r$, where the induction rules are these of $\createdByStar{_}$.

  1989  \end{proof}

  1990 % The simplification of a flattened out regular expression, provided it comes

  1991 %from the derivative of a star, is the same as the one nested.

  1992