equal
deleted
inserted
replaced
1351 \end{center} |
1351 \end{center} |
1352 |
1352 |
1353 % tell Chengsong about Indian paper of closed forms of derivatives |
1353 % tell Chengsong about Indian paper of closed forms of derivatives |
1354 |
1354 |
1355 \noindent |
1355 \noindent |
1356 where in (1) the $\textit{Suffix}(@{text "r"}_1, s)$ are the all the suffixes of $s$ where @{term "bders_simp r\<^sub>1 s'"} is nullable ($s'$ being a suffix of $s$). |
1356 where in (1) the $\textit{Suffix}(@{text "r"}_1, s)$ are all the suffixes of $s$ where @{term "bders_simp r\<^sub>1 s'"} is nullable ($s'$ being a suffix of $s$). |
1357 In (3) we know that $\llbracket@{term "ASEQ [] (bders_simp r\<^sub>1 s) r\<^sub>2"}\rrbracket$ is |
1357 In (3) we know that $\llbracket@{term "ASEQ [] (bders_simp r\<^sub>1 s) r\<^sub>2"}\rrbracket$ is |
1358 bounded by $N_1 + \llbracket{}r_2\rrbracket + 1$. In (5) we know the list comprehension contains only regular expressions of size smaller |
1358 bounded by $N_1 + \llbracket{}r_2\rrbracket + 1$. In (5) we know the list comprehension contains only regular expressions of size smaller |
1359 than $N_2$. The list length after @{text distinctWith} is bounded by a number, which we call $l_{N_2}$. It stands |
1359 than $N_2$. The list length after @{text distinctWith} is bounded by a number, which we call $l_{N_2}$. It stands |
1360 for the number of distinct regular expressions smaller than $N_2$ (there can only be finitely many of them). |
1360 for the number of distinct regular expressions smaller than $N_2$ (there can only be finitely many of them). |
1361 We reason similarly for @{text STAR}.\smallskip |
1361 We reason similarly for @{text STAR}.\smallskip |