equal
deleted
inserted
replaced
1 theory Myhill |
1 theory Myhill |
2 imports Main List_Prefix Prefix_subtract |
2 imports Main List_Prefix Prefix_subtract |
3 begin |
3 begin |
|
4 |
|
5 (* |
|
6 text {* |
|
7 \begin{figure} |
|
8 \centering |
|
9 \scalebox{0.95}{ |
|
10 \begin{tikzpicture}[->,>=latex,shorten >=1pt,auto,node distance=1.2cm, semithick] |
|
11 \node[state,initial] (n1) {$1$}; |
|
12 \node[state,accepting] (n2) [right = 10em of n1] {$2$}; |
|
13 |
|
14 \path (n1) edge [bend left] node {$0$} (n2) |
|
15 (n1) edge [loop above] node{$1$} (n1) |
|
16 (n2) edge [loop above] node{$0$} (n2) |
|
17 (n2) edge [bend left] node {$1$} (n1) |
|
18 ; |
|
19 \end{tikzpicture}} |
|
20 \caption{An example automaton (or partition)}\label{fig:example_automata} |
|
21 \end{figure} |
|
22 *} |
|
23 |
|
24 *) |
4 |
25 |
5 section {* Preliminary definitions *} |
26 section {* Preliminary definitions *} |
6 |
27 |
7 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *} |
28 text {* Sequential composition of two languages @{text "L1"} and @{text "L2"} *} |
8 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |
29 definition Seq :: "string set \<Rightarrow> string set \<Rightarrow> string set" ("_ ;; _" [100,100] 100) |