equal
deleted
inserted
replaced
26 "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _ | _})") |
26 "_CollectIn" :: "pttrn => 'a set => bool => 'a set" ("(1{_ \<in> _ | _})") |
27 translations |
27 translations |
28 "_Collect p P" <= "{p. P}" |
28 "_Collect p P" <= "{p. P}" |
29 "_Collect p P" <= "{p|xs. P}" |
29 "_Collect p P" <= "{p|xs. P}" |
30 "_CollectIn p A P" <= "{p : A. P}" |
30 "_CollectIn p A P" <= "{p : A. P}" |
|
31 |
|
32 syntax (latex output) |
|
33 "_UNION_le" :: "'a \<Rightarrow> 'a => 'b set => 'b set" ("(3\<Union>(00\<^bsub>_ \<le> _\<^esub>)/ _)" [0, 0, 10] 10) |
31 |
34 |
32 abbreviation "ZERO \<equiv> Zero" |
35 abbreviation "ZERO \<equiv> Zero" |
33 abbreviation "ONE \<equiv> One" |
36 abbreviation "ONE \<equiv> One" |
34 abbreviation "ATOM \<equiv> Atom" |
37 abbreviation "ATOM \<equiv> Atom" |
35 abbreviation "PLUS \<equiv> Plus" |
38 abbreviation "PLUS \<equiv> Plus" |
2461 our formalisation can be found in the Archive of Formal Proofs at |
2464 our formalisation can be found in the Archive of Formal Proofs at |
2462 \mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip |
2465 \mbox{\url{http://afp.sourceforge.net/devel-entries/Myhill-Nerode.shtml}} \cite{myhillnerodeafp11}.\medskip |
2463 |
2466 |
2464 \noindent |
2467 \noindent |
2465 {\bf Acknowledgements:} |
2468 {\bf Acknowledgements:} |
2466 We are grateful for the comments we received from Larry |
2469 We are grateful for the comments we received from Larry Paulson. Tobias |
2467 Paulson, Tobias Nipkow made us aware of the properties in Lemma~\ref{subseqreg} |
2470 Nipkow made us aware of the properties in Lemma~\ref{subseqreg} and Tjark |
2468 and Tjark Weber helped us with their proofs. |
2471 Weber helped us with their proofs. |
|
2472 |
2469 |
2473 |
2470 *} |
2474 *} |
2471 |
2475 |
2472 |
2476 |
2473 (*<*) |
2477 (*<*) |