]> 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.
 
 (*
 // qed.
 
 (*
-Example. Let us consider the item                      
+\ 5b\ 6Example\ 5/b\ 6. Let us consider the item                      
   
                                (•a + ϵ)((•b)*•a + •b)b
 
   
                                (•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.
 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)*.
 
 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.
 
 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.
 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.
 
 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$ 
 
 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$