commit by user andrea

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index fb11216e53fb538d84099769257b5e77045687f2..c9a65f57b0935ee4774b84ce39f5f1767690f977 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -107,42 +107,42 @@ qed.
 
 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 
-let rec moves (S : DeqSet) w e on w : pre S ≝
+let rec moves (S : \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) w e on w : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
  match w with
   [ nil ⇒ e
-  | cons x w' ⇒ w' ↦* (move S x (\fst e))]. 
+  | cons x w' ⇒ w' ↦* (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e))]. 
 
-lemma moves_empty: ∀S:DeqSet.∀e:pre S. 
-  moves ? [ ] e = e.
+lemma moves_empty: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+  \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ] e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 e.
 // qed.
 
-lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S. 
-  moves ? (a::w)  e = moves ? w (move S a (\fst e)).
+lemma moves_cons: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+  \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w)  e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e)).
 // qed.
 
 lemma moves_left : ∀S,a,w,e. 
-  moves S (w@[a]) e = move S a (\fst (moves S w e)). 
-#S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
+  \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S (w\ 5a title="append" href="cic:/fakeuri.def(1)"\ 6@\ 5/a\ 6\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6a]) e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e)). 
+#S #a #w elim w // #x #tl #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 //
 qed.
 
-lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S. 
-  iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
+lemma not_epsilon_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+  \ 5a href="cic:/matita/basics/logic/iff.def(1)"\ 6iff\ 5/a\ 6 ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_prl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 e) ((a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w) \ 5a title="in_pl mem" href="cic:/fakeuri.def(1)"\ 6∈\ 5/a\ 6 \ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
 #S #a #w * #i #b cases b normalize 
-  [% /2/ * // #H destruct |% normalize /2/]
+  [% /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,1,2)"\ 6or_introl\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ * // #H destruct |% normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5/span\ 6\ 5/span\ 6/]
 qed.
 
-lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
-  |\fst (moves ? w e)| = |\fst e|.
+lemma same_kernel_moves: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w.∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S.
+  \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e)| \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e|.
 #S #w elim w //
 qed.
 
-theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S. 
-   (\snd (moves ? w e) = true) ↔ \sem{e} w.
+theorem decidable_sem: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S. ∀e:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. 
+   (\ 5a title="pair pi2" href="cic:/fakeuri.def(1)"\ 6\snd\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 ? w e) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/basics/bool/bool.con(0,1,0)"\ 6true\ 5/a\ 6) \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{e} w.
 #S #w elim w 
- [* #i #b >moves_empty cases b % /2/
- |#a #w1 #Hind #e >moves_cons
-  @iff_trans [||@iff_sym @not_epsilon_sem]
-  @iff_trans [||@move_ok] @Hind
+ [* #i #b >\ 5a href="cic:/matita/tutorial/chapter9/moves_empty.def(8)"\ 6moves_empty\ 5/a\ 6 cases b % /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/tutorial/chapter7/true_to_epsilon.def(9)"\ 6true_to_epsilon\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/\ 5span class="error" title="error location"\ 6\ 5/span\ 6 #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/absurd.def(2)"\ 6absurd\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
+ |#a #w1 #Hind #e >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6
+  @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/basics/logic/iff_sym.def(2)"\ 6iff_sym\ 5/a\ 6 @\ 5a href="cic:/matita/tutorial/chapter9/not_epsilon_sem.def(9)"\ 6not_epsilon_sem\ 5/a\ 6]
+  @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6 [||@\ 5a href="cic:/matita/tutorial/chapter9/move_ok.def(14)"\ 6move_ok\ 5/a\ 6] @Hind
  ]
 qed.
 
@@ -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="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/\ 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,14 +176,13 @@ 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 
+\ 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 
+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