1 \documentclass[a4paper,UKenglish]{lipics} |
1 \documentclass[a4paper,UKenglish]{lipics} |
2 \usepackage{graphic} |
2 \usepackage{graphic} |
3 \usepackage{data} |
3 \usepackage{data} |
4 \usepackage{tikz-cd} |
4 \usepackage{tikz-cd} |
5 \usepackage{tikz} |
5 \usepackage{tikz} |
6 \usetikzlibrary{graphs} |
6 |
7 \usetikzlibrary{graphdrawing} |
7 %\usetikzlibrary{graphs} |
8 \usegdlibrary{trees} |
8 %\usetikzlibrary{graphdrawing} |
|
9 %\usegdlibrary{trees} |
|
10 |
9 %\usepackage{algorithm} |
11 %\usepackage{algorithm} |
10 \usepackage{amsmath} |
12 \usepackage{amsmath} |
11 \usepackage{xcolor} |
13 \usepackage{xcolor} |
12 \usepackage[noend]{algpseudocode} |
14 \usepackage[noend]{algpseudocode} |
13 \usepackage{enumitem} |
15 \usepackage{enumitem} |
1549 we say that the regular expression $r$ contains |
1551 we say that the regular expression $r$ contains |
1550 the bitcode $\textit{bs}$, written |
1552 the bitcode $\textit{bs}$, written |
1551 $r \gg \textit{bs}$. |
1553 $r \gg \textit{bs}$. |
1552 The $\gg$ operator with the |
1554 The $\gg$ operator with the |
1553 regular expression $r$ may also be seen as a |
1555 regular expression $r$ may also be seen as a |
1554 |
1556 regular language by itself on the alphabet |
1555 \end{tikzpicture} |
1557 $\Sigma = {0,1}$. |
1556 \end{center} |
1558 The definition of contains relation |
|
1559 is given in an inductive form, similar to that |
|
1560 of regular expressions, it might not be surprising |
|
1561 that the set it denotes contains basically |
|
1562 everything a regular expression can |
|
1563 produce during the derivative and lexing process. |
|
1564 This can be seen in the subsequent lemmas we have |
|
1565 proved about contains: |
|
1566 \begin{itemize} |
|
1567 \item |
|
1568 $\textit{if} \models v:r \; \textit{then} \; \rup \gg \textit{code}(v)$ |
|
1569 \end{itemize} |
1557 \subsection{the $\textit{ders}_2$ Function} |
1570 \subsection{the $\textit{ders}_2$ Function} |
1558 If we want to prove the result |
1571 If we want to prove the result |
1559 \begin{center} |
1572 \begin{center} |
1560 $ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$ |
1573 $ \textit{blexer}\_{simp}(r, \; s) = \textit{blexer}(r, \; s)$ |
1561 \end{center} |
1574 \end{center} |