]> matita.cs.unibo.it Git - helm.git/commitdiff
Pictures
authormatitaweb <claudio.sacerdoticoen@unibo.it>
Tue, 6 Mar 2012 12:45:54 +0000 (12:45 +0000)
committermatitaweb <claudio.sacerdoticoen@unibo.it>
Tue, 6 Mar 2012 12:45:54 +0000 (12:45 +0000)
weblib/tutorial/acUbc.gif [new file with mode: 0644]
weblib/tutorial/chapter9.ma

diff --git a/weblib/tutorial/acUbc.gif b/weblib/tutorial/acUbc.gif
new file mode 100644 (file)
index 0000000..5812fc8
Binary files /dev/null and b/weblib/tutorial/acUbc.gif differ
index 6126269d8d56be07b47a03557e2e9be8ee287d41..c68c8f1a0e978c2188fd53ef313c7a3c0e355501 100644 (file)
@@ -34,7 +34,7 @@ lemma move_star: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6
 // qed.
 
 (*
-Example. Let us consider the item                      
+\ 5b\ 6Example\ 5/b\ 6. 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.
+
+\ 5b\ 6Example\ 5/b\ 6
 Below is the DFA associated with the regular expression (ac+bc)*.
 
-\includegraphics[width=.8\textwidth]{acUbc.pdf}
-\caption{DFA for $(ac+bc)^*$\label{acUbc}}
+\ 5img src="acUbc.gif" alt="some_text"/\ 6  
 
 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.
+
+\ 5b\ 6Example\ 5/b\ 6
 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}}
+\ 5img src="automaton.pdf" alt="some_text"/\ 6 
 
 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$