starl

[helm.git] / weblib / tutorial / chapter9.ma

diff --git a/weblib/tutorial/chapter9.ma b/weblib/tutorial/chapter9.ma
index 6126269d8d56be07b47a03557e2e9be8ee287d41..13a0526b1328dd21b1c2f2dea291b4713fc15df5 100644 (file)
--- a/weblib/tutorial/chapter9.ma
+++ b/weblib/tutorial/chapter9.ma
@@ -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
 


@@ -107,42 +107,42 @@ qed.
 
 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 
 
 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
  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.
 
 // 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. 
 // 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(a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 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 \ 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.
 
 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 
 #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.
 
 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.
 
 #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 
 #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.
 
  ]
 qed.
 


@@ -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="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.
 
 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,63 +172,79 @@ 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="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 
 
 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 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. *)

 
 

-(************************ pit state ***************************)
-definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉. 
+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 href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6〉. 

 
 

-let rec occur (S: DeqSet) (i: re S) on i ≝  
+(* 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 ≝  

   match i with
   match i with

-  [ z ⇒ [ ]
-  | e ⇒ [ ]
-  | s y ⇒ [y]
-  | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
-  | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2) 
+  [ z ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+  | e ⇒ \ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6 ]
+  | s y ⇒ y\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:\ 5a title="nil" href="cic:/fakeuri.def(1)"\ 6[\ 5/a\ 6]
+  | o e1 e2 ⇒ \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (occur S e1) (occur S e2) 
+  | c e1 e2 ⇒ \ 5a href="cic:/matita/tutorial/chapter5/unique_append.fix(0,1,5)"\ 6unique_append\ 5/a\ 6 ? (occur S e1) (occur S e2) 

   | k e ⇒ occur S e].
 
   | k e ⇒ occur S e].
 

-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.
+(* 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:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 5/a\ 6 S (\ 5a title="forget" href="cic:/fakeuri.def(1)"\ 6|\ 5/a\ 6i|)) \ 5a title="leibnitz's non-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 href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S a i  \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.

 #S #a #i elim i //
 #S #a #i elim i //

-  [#x normalize cases (a==x) normalize // #H @False_ind /2/
-  |#i1 #i2 #Hind1 #Hind2 #H >move_cat 
-   >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
-   >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
-  |#i1 #i2 #Hind1 #Hind2 #H >move_plus 
-   >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
-   >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
-  |#i #Hind #H >move_star >Hind // 
+  [#x normalize cases (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x) normalize // #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/
+  |#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 
+   >Hind1 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 //]
+   >Hind2 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 //] //
+  |#i1 #i2 #Hind1 #Hind2 #H >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 
+   >Hind1 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l1.def(6)"\ 6sublist_unique_append_l1\ 5/a\ 6 //]
+   >Hind2 [2:@(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 @\ 5a href="cic:/matita/tutorial/chapter5/sublist_unique_append_l2.def(6)"\ 6sublist_unique_append_l2\ 5/a\ 6 //] //
+  |#i #Hind #H >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6 >Hind // 

   ]
 qed.
 
   ]
 qed.
 

-lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
+(* We cannot escape form the pit state. *)
+
+lemma move_pit: ∀S,a,i. \ 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/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i)) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.

 #S #a #i elim i //
 #S #a #i elim i //

-  [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 // 
-  |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 // 
-  |#i #Hind >move_star >Hind //
+  [#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 >Hind1 >Hind2 // 
+  |#i1 #i2 #Hind1 #Hind2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 >Hind1 >Hind2 // 
+  |#i #Hind >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6 >Hind //

   ]
 qed. 
 
   ]
 qed. 
 

-lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
+lemma moves_pit: ∀S,w,i. \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i) \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S i.

 #S #w #i elim w // 
 qed. 
  
 #S #w #i elim w // 
 qed. 
  

-lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
- moves S w e = pit_pre S (\fst e).
+(* 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. \ 5a title="logical not" href="cic:/fakeuri.def(1)"\ 6¬\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter5/sublist.def(5)"\ 6sublist\ 5/a\ 6 S w (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 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 e|)) →
+ \ 5a href="cic:/matita/tutorial/chapter9/moves.fix(0,1,7)"\ 6moves\ 5/a\ 6 S w e \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter9/pit_pre.def(4)"\ 6pit_pre\ 5/a\ 6 S (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).

 #S #w elim w
 #S #w elim w

-  [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
-  |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
-    [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a) 
-     @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
+  [#e * #H @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 @H normalize #a #abs @\ 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 #tl #Hind #e #H cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter5/memb.fix(0,2,4)"\ 6memb\ 5/a\ 6 S a (\ 5a href="cic:/matita/tutorial/chapter9/occur.fix(0,1,6)"\ 6occur\ 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 e|))))
+    [#Htrue >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 whd in ⊢ (???%); <(\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 … a) 
+     @Hind >\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 @(\ 5a href="cic:/matita/basics/logic/not_to_not.def(3)"\ 6not_to_not\ 5/a\ 6 … H) #H1 #b #memb cases (\ 5a href="cic:/matita/basics/bool/orb_true_l.def(2)"\ 6orb_true_l\ 5/a\ 6 … memb)

       [#H2 >(\P H2) // |#H2 @H1 //]
       [#H2 >(\P H2) // |#H2 @H1 //]

-    |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/ 
+    |#Hfalse >\ 5a href="cic:/matita/tutorial/chapter9/moves_cons.def(8)"\ 6moves_cons\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter9/not_occur_to_pit.def(8)"\ 6not_occur_to_pit\ 5/a\ 6 // >Hfalse /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/bool/eqnot_to_noteq.def(4)"\ 6eqnot_to_noteq\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/ 

     ]
   ]
     ]
   ]

-qed.
\ No newline at end of file
+qed.