From: matitaweb Date: Tue, 6 Mar 2012 12:45:54 +0000 (+0000) Subject: Pictures X-Git-Tag: make_still_working~1903 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=faf5a856ba919cb1eb6a24331601d57940c41eff;p=helm.git Pictures --- diff --git a/weblib/tutorial/acUbc.gif b/weblib/tutorial/acUbc.gif new file mode 100644 index 000000000..5812fc8f4 Binary files /dev/null and b/weblib/tutorial/acUbc.gif differ diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma index 6126269d8..c68c8f1a0 100644 --- a/weblib/tutorial/chapter9.ma +++ b/weblib/tutorial/chapter9.ma @@ -34,7 +34,7 @@ lemma move_star: ∀S:a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)" // qed. (* -Example. Let us consider the item +bExample/b. Let us consider the item (•a + ϵ)((•b)*•a + •b)b @@ -154,10 +154,11 @@ e. This is one of the advantages of pointed regular expressions w.r.t. derivativ whose finite nature only holds after a suitable quotient. Let us discuss a couple of examples. + +bExample/b. Below is the DFA associated with the regular expression (ac+bc)*. -\includegraphics[width=.8\textwidth]{acUbc.pdf} -\caption{DFA for $(ac+bc)^*$\label{acUbc}} +img src="acUbc.gif" alt="some_text"/ The graphical description of the automaton is the traditional one, with nodes for states and labelled arcs for transitions. Unreachable states are not shown. @@ -171,10 +172,11 @@ behaviour of the automaton. As a consequence, the construction of the automaton only direct, but also extremely intuitive and locally verifiable. Let us consider a more complex case. + +bExample/b. Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton. -\includegraphics[width=.8\textwidth]{automaton.pdf} -\caption{DFA for $(a+\epsilon)(b^*a + b)b$\label{automaton}} +img src="automaton.pdf" alt="some_text"/ Remarkably, this DFA is minimal, testifying the small number of states produced by our technique (the pair ofstates $6-8$ and $7-9$ differ for the fact that $6$ and $7$