chapter 9

diff --git a/weblib/tutorial/acUbc.gif b/weblib/tutorial/acUbc.gif
index 5812fc8f462a99d6f138ae01d7758fca10b2bd8f..9222a3418585ed44c08c9d813cd7f6b8603d1d41 100644 (file)
Binary files a/weblib/tutorial/acUbc.gif and b/weblib/tutorial/acUbc.gif differ

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index c68c8f1a0e978c2188fd53ef313c7a3c0e355501..fb11216e53fb538d84099769257b5e77045687f2 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -158,7 +158,7 @@ Let us discuss a couple of examples.
 \ 5b\ 6Example\ 5/b\ 6. 
 Below is the DFA associated with the regular expression (ac+bc)*.
 
-\ 5img src="acUbc.gif" alt="some_text"/\ 6  
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/\ 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.
@@ -176,16 +176,24 @@ 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.
 
-\ 5img src="automaton.pdf" alt="some_text"/\ 6 
+\ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"/\ 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$ 
-are final, while $8$ and $9$ are not). 
+technique (the pair ofstates 6-8 and 7-9 differ for the fact that 6 and 7 
+are final, while 8 and 9 are not). 
 *) 
 
-(************************ pit state ***************************)
+(*
+\ 5h2\ 6Move to pit\ 5/h2\ 6. 
+
+We conclude this chapter with a few properties of the move opertions in relation
+with the pit state. *).
+
 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
 
+(* The following function compute if a symbol in S occurs in a given
+item i *).
+
 let rec occur (S: DeqSet) (i: re S) on i ≝  
   match i with
   [ z ⇒ [ ]
@@ -195,6 +203,9 @@ let rec occur (S: DeqSet) (i: re S) on i ≝
   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
   | k e ⇒ occur S e].
 
+(* If a symbol a does not occur in i, then move(i,a) gets to the
+pit state. *).
+
 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
   move S a i  = pit_pre S i.
 #S #a #i elim i //
@@ -209,6 +220,8 @@ lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true 
   ]
 qed.
 
+(* We cannot escape form the pit state. *).
+
 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
 #S #a #i elim i //
   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 
@@ -221,6 +234,9 @@ lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
 #S #w #i elim w // 
 qed. 
  
+(* If any character in w does not occur in i, then moves(i,w) gets
+to the pit state. *).
+
 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
  moves S w e = pit_pre S (\fst e).
 #S #w elim w