1432 \noindent |
1432 \noindent |
1433 From this we get a corollary that |
1433 From this we get a corollary that |
1434 if forall $r \in rs$, $\rsize{r} \leq N$, then the output of |
1434 if forall $r \in rs$, $\rsize{r} \leq N$, then the output of |
1435 $\rdistinct{rs}{\varnothing}$ is a list of regular |
1435 $\rdistinct{rs}{\varnothing}$ is a list of regular |
1436 expressions of finite size depending on $N$ only. |
1436 expressions of finite size depending on $N$ only. |
1437 \begin{corollary} |
1437 \begin{corollary}\label{finiteSizeNCorollary} |
1438 Assumes that for all $r \in rs. \rsize{r} \leq N$, |
1438 Assumes that for all $r \in rs. \rsize{r} \leq N$, |
1439 and the cardinality of $\sizeNregex \; N$ is $c_N$ |
1439 and the cardinality of $\sizeNregex \; N$ is $c_N$ |
1440 then$\rsize{\rdistinct{rs}{\varnothing}} \leq c*N$. |
1440 then$\rsize{\rdistinct{rs}{\varnothing}} \leq c*N$. |
1441 \end{corollary} |
1441 \end{corollary} |
1442 \noindent |
1442 \noindent |
1485 $\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$. We can reason as follows |
1485 $\exists N_2. \forall s. \; \llbracket \rderssimp{r_2}{s} \rrbracket \leq N_2$. We can reason as follows |
1486 % |
1486 % |
1487 \begin{center} |
1487 \begin{center} |
1488 \begin{tabular}{lcll} |
1488 \begin{tabular}{lcll} |
1489 & & $ \llbracket \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\ |
1489 & & $ \llbracket \rderssimp{r_1\cdot r_2 }{s} \rrbracket_r $\\ |
1490 & $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash s \cdot r_2 \; \; :: \; \; |
1490 & $ = $ & $\llbracket \rsimp{(\sum(r_1 \backslash_{rsimp} s \cdot r_2 \; \; :: \; \; |
1491 \map \; (\lambda s'. r_2\backslash_{rsimp} s') (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\ |
1491 \map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r})))} \rrbracket_r $ & (1) \\ |
1492 & $\leq$ & $\llbracket \rsimp{(\sum(r_1 \backslash s \cdot r_2 :: |
1492 & $\leq$ & $\llbracket \rdistinct{(r_1 \backslash_{rsimp} s \cdot r_2 \; \; :: \; \; |
1493 \map \; (\lambda s'. r_2\backslash_{rsimp} s') (\vsuf{s}{r})))} \rrbracket_r $ & (2) \\ |
1493 \map \; (r_2\backslash_{rsimp} \_)\; (\vsuf{s}{r}))}{\varnothing} \rrbracket_r + 1$ & (2) \\ |
1494 |
1494 & $\leq$ & $2 + N_1 + \rsize{r_2} + (N_2 * (card\;(\sizeNregex \; N_2)))$ & (3)\\ |
|
1495 $\rsize{(r_1 \cdot r_2) \backslash_r s}$& $\leq$ & $max \; (2 + N_1 + \llbracket r_2 \rrbracket_r + N_2 * (card\; (\sizeNregex \; N_2))) \; \rsize{r_1\cdot r_2}$ & (4) |
1495 \end{tabular} |
1496 \end{tabular} |
1496 \end{center} |
1497 \end{center} |
1497 |
1498 \noindent |
1498 \end{proof} |
1499 (1) is by the corollary \ref{seqEstimate1}. |
1499 |
1500 (2) is by \ref{altsSimpControl}. |
1500 \noindent |
1501 (3) is by \ref{finiteSizeNCorollary}. |
1501 (1) is by the corollary \ref{seqEstimate1} |
1502 (4) is by splitting the case when $s = []$ and $s \neq []$. |
1502 The term (2) is used to control (1). |
1503 |
1503 That is because one can obtain an overall |
|
1504 smaller regex list |
|
1505 by flattening it and removing $\ZERO$s first before applying $\distinctWith$ on it. |
|
1506 Section 3 is dedicated to its proof. |
|
1507 In (3) we know that $\llbracket \ASEQ{bs}{(\rderssimp{ r_1}{s}}{r_2}\rrbracket$ is |
|
1508 bounded by $N_1 + \llbracket{}r_2\rrbracket + 1$. In (5) we know the list comprehension contains only regular expressions of size smaller |
|
1509 than $N_2$. The list length after $\distinctWith$ is bounded by a number, which we call $l_{N_2}$. It stands |
|
1510 for the number of distinct regular expressions smaller than $N_2$ (there can only be finitely many of them). |
|
1511 We reason similarly for $\STAR$.\medskip |
1504 We reason similarly for $\STAR$.\medskip |
|
1505 \end{proof} |
|
1506 |
|
1507 \noindent |
1512 |
1508 |
1513 %----------------------------------- |
1509 %----------------------------------- |
1514 % SECTION 2 |
1510 % SECTION 2 |
1515 %----------------------------------- |
1511 %----------------------------------- |
1516 |
1512 |