equal
deleted
inserted
replaced
1044 \ref{grewritesSimpalts}, \ref{gstarRdistinctGeneral}, \ref{rderRsimpAltsCommute}, and |
1044 \ref{grewritesSimpalts}, \ref{gstarRdistinctGeneral}, \ref{rderRsimpAltsCommute}, and |
1045 \ref{insideSimpRemoval}. |
1045 \ref{insideSimpRemoval}. |
1046 \end{proof} |
1046 \end{proof} |
1047 \noindent |
1047 \noindent |
1048 This closed form has a variant which can be more convenient in later proofs: |
1048 This closed form has a variant which can be more convenient in later proofs: |
1049 \begin{corollary} |
1049 \begin{corollary}{altsClosedForm1} |
1050 If $s \neq []$ then |
1050 If $s \neq []$ then |
1051 $\rderssimp \; (\sum \; rs) \; s = |
1051 $\rderssimp \; (\sum \; rs) \; s = |
1052 \rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$. |
1052 \rsimp{(\sum \; (\map \; \rderssimp{\_}{s} \; rs))}$. |
1053 \end{corollary} |
1053 \end{corollary} |
1054 \noindent |
1054 \noindent |
1496 \end{center} |
1496 \end{center} |
1497 |
1497 |
1498 \end{proof} |
1498 \end{proof} |
1499 |
1499 |
1500 \noindent |
1500 \noindent |
1501 where in (1) the $\textit{Suffix}( r_1, s)$ are the all the suffixes of $s$ where $\rderssimp{ r_1}{s'}$ is nullable ($s'$ being a suffix of $s$). |
1501 (1) is by the corollary \ref{seqEstimate1} |
1502 The reason why we could write the derivatives of a sequence this way is described in section 2. |
|
1503 The term (2) is used to control (1). |
1502 The term (2) is used to control (1). |
1504 That is because one can obtain an overall |
1503 That is because one can obtain an overall |
1505 smaller regex list |
1504 smaller regex list |
1506 by flattening it and removing $\ZERO$s first before applying $\distinctWith$ on it. |
1505 by flattening it and removing $\ZERO$s first before applying $\distinctWith$ on it. |
1507 Section 3 is dedicated to its proof. |
1506 Section 3 is dedicated to its proof. |