+\ 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.
+Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
+only if b is true, we may just label nodes with the item.
+The automaton is not minimal: it is easy to see that the two states corresponding to
+the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
+that they define the same language!). In fact, an important property of pres e is that
+each state has a clear semantics, given in terms of the specification e and not of the
+behaviour of the automaton. As a consequence, the construction of the automaton is not
+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.
+
+\ 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 of states 6-8 and 7-9 differ for the fact that 6 and 7
+are final, while 8 and 9 are not).
+
+
+\ 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.\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6\ 5a href="cic:/matita/tutorial/chapter8/blank.fix(0,1,3)"\ 6blank\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6), \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6\ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〉\ 5/a\ 6.
+
+(* The following function compute the list of characters occurring in a given
+item i. *)
+
+let rec occur (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (i: \ 5a href="cic:/matita/tutorial/chapter7/re.ind(1,0,1)"\ 6re\ 5/a\ 6 S) on i ≝