weblib/tutorial/chapter9.ma

   1 (*
   2 \ 5h1\ 6Moves\ 5/h1\ 6We now define the move operation, that corresponds to the advancement of the
   3 state in response to the processing of an input character a. The intuition is
   4 clear: we have to look at points inside $e$ preceding the given character a,
   5 let the point traverse the character, and broadcast it. All other points must
   6 be removed.
   7
   8 We can give a particularly elegant definition in terms of the
   9 lifted operators of the previous section:
  10 *)
  11
  12 include "tutorial/chapter8.ma".
  13
  14 let rec move (S: \ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6) (x:S) (E: \ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S) on E : \ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S ≝
  15  match E with
  16   [ pz ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a href="cic:/matita/tutorial/chapter7/pitem.con(0,1,1)"\ 6pz\ 5/a\ 6 S, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
  17   | pe ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem epsilon" href="cic:/fakeuri.def(1)"\ 6ϵ\ 5/a\ 6, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
  18   | ps y ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y, \ 5a href="cic:/matita/basics/bool/bool.con(0,2,0)"\ 6false\ 5/a\ 6 〉
  19   | pp y ⇒ \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6 \ 5a title="pitem ps" href="cic:/fakeuri.def(1)"\ 6`\ 5/a\ 6y, x \ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6= y 〉
  20   | po e1 e2 ⇒ (move ? x e1) \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 (move ? x e2)
  21   | pc e1 e2 ⇒ (move ? x e1) \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 (move ? x e2)
  22   | pk e ⇒ (move ? x e)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛ ].
  23
  24 lemma move_plus: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
  25   \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (i1 \ 5a title="pitem or" href="cic:/fakeuri.def(1)"\ 6+\ 5/a\ 6 i2) \ 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 ? x i1) \ 5a title="oplus" href="cic:/fakeuri.def(1)"\ 6⊕\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i2).
  26 // qed.
  27
  28 lemma move_cat: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i1,i2:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
  29   \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x (i1 \ 5a title="pitem cat" href="cic:/fakeuri.def(1)"\ 6·\ 5/a\ 6 i2) \ 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 ? x i1) \ 5a title="lifted cat" href="cic:/fakeuri.def(1)"\ 6⊙\ 5/a\ 6 (\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x i2).
  30 // qed.
  31
  32 lemma move_star: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
  33   \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 S x i\ 5a title="pitem star" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6* \ 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 ? x i)\ 5a title="lk" href="cic:/fakeuri.def(1)"\ 6^\ 5/a\ 6⊛.
  34 // qed.
  35
  36 (*
  37 \ 5b\ 6Example\ 5/b\ 6. Let us consider the item
  38
  39                                (•a + ϵ)((•b)*•a + •b)b
  40
  41 and the two moves w.r.t. the characters a and b.
  42 For a, we have two possible positions (all other points gets erased); the innermost
  43 point stops in front of the final b, while the other one broadcast inside (b^*a + b)b,
  44 so
  45
  46       move((•a + ϵ)((•b)*•a + •b)b,a) = 〈(a + ϵ)((•b)^*•a + •b)•b, false〉
  47
  48 For b, we have two positions too. The innermost point stops in front of the final b too,
  49 while the other point reaches the end of b* and must go back through b*a:
  50
  51       move((•a + ϵ)((•b)*•a + •b)b ,b) = 〈(a +  ϵ)((•b)*•a + b)•b, false〉
  52
  53 *)
  54
  55 definition pmove ≝ λS:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.λx:S.λe:\ 5a href="cic:/matita/tutorial/chapter7/pre.def(1)"\ 6pre\ 5/a\ 6 S. \ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? x (\ 5a title="pair pi1" href="cic:/fakeuri.def(1)"\ 6\fst\ 5/a\ 6 e).
  56
  57 lemma pmove_def : ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀x:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀b.
  58   \ 5a href="cic:/matita/tutorial/chapter9/pmove.def(7)"\ 6pmove\ 5/a\ 6 ? x \ 5a title="Pair construction" href="cic:/fakeuri.def(1)"\ 6〈\ 5/a\ 6i,b〉 \ 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 ? x i.
  59 // qed.
  60
  61 lemma eq_to_eq_hd: ∀A.∀l1,l2:\ 5a href="cic:/matita/basics/list/list.ind(1,0,1)"\ 6list\ 5/a\ 6 A.∀a,b.
  62   a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l1 \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:l2 → a \ 5a title="leibnitz's equality" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6 b.
  63 #A #l1 #l2 #a #b #H destruct //
  64 qed.
  65
  66 (* Obviously, a move does not change the carrier of the item, as one can easily
  67 prove by induction on the item. *)
  68
  69 lemma same_kernel: ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.
  70   \ 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/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a i)| \ 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\ 6i|.
  71 #S #a #i elim i //
  72   [#i1 #i2 #H1 #H2 >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter8/erase_odot.def(7)"\ 6erase_odot\ 5/a\ 6 //
  73   |#i1 #i2 #H1 #H2 >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 whd in ⊢ (??%%); //
  74   ]
  75 qed.
  76
  77 (* Here is our first, major result, stating the correctness of the
  78 move operation. The proof is a simple induction on i. *)
  79
  80 theorem move_ok:
  81  ∀S:\ 5a href="cic:/matita/tutorial/chapter4/DeqSet.ind(1,0,0)"\ 6DeqSet\ 5/a\ 6.∀a:S.∀i:\ 5a href="cic:/matita/tutorial/chapter7/pitem.ind(1,0,1)"\ 6pitem\ 5/a\ 6 S.∀w: \ 5a href="cic:/matita/tutorial/chapter6/word.def(3)"\ 6word\ 5/a\ 6 S.
  82    \ 5a title="in_prl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{\ 5a href="cic:/matita/tutorial/chapter9/move.fix(0,2,6)"\ 6move\ 5/a\ 6 ? a i} w \ 5a title="iff" href="cic:/fakeuri.def(1)"\ 6↔\ 5/a\ 6 \ 5a title="in_pl" href="cic:/fakeuri.def(1)"\ 6\sem\ 5/a\ 6{i} (a\ 5a title="cons" href="cic:/fakeuri.def(1)"\ 6:\ 5/a\ 6:w).
  83 #S #a #i elim i
  84   [normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  85   |normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  86   |normalize /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/And.con(0,1,2)"\ 6conj\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/
  87   |normalize #x #w cases (\ 5a href="cic:/matita/basics/bool/true_or_false.def(1)"\ 6true_or_false\ 5/a\ 6 (a\ 5a title="eqb" href="cic:/fakeuri.def(1)"\ 6=\ 5/a\ 6=x)) #H >H normalize
  88     [>(\P H) % [* // #bot @\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 //| #H1 destruct /\ 5span class="autotactic"\ 62\ 5span class="autotrace"\ 6 trace \ 5a href="cic:/matita/basics/logic/Or.con(0,2,2)"\ 6or_intror\ 5/a\ 6\ 5/span\ 6\ 5/span\ 6/]
  89     |% [@\ 5a href="cic:/matita/basics/logic/False_ind.fix(0,1,1)"\ 6False_ind\ 5/a\ 6 |#H1 cases (\Pf H) #H2 @H2 destruct //]
  90     ]
  91   |#i1 #i2 #HI1 #HI2 #w >\ 5a href="cic:/matita/tutorial/chapter9/move_cat.def(7)"\ 6move_cat\ 5/a\ 6
  92    @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6[|@\ 5a href="cic:/matita/tutorial/chapter8/sem_odot.def(13)"\ 6sem_odot\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_cat_w.def(8)"\ 6sem_cat_w\ 5/a\ 6
  93    @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6[||@(\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"\ 6iff_or_l\ 5/a\ 6 … (HI2 w))] @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6
  94    @\ 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/chapter6/deriv_middot.def(5)"\ 6deriv_middot\ 5/a\ 6 //]
  95    @\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 @HI1
  96   |#i1 #i2 #HI1 #HI2 #w >(\ 5a href="cic:/matita/tutorial/chapter7/sem_plus.def(8)"\ 6sem_plus\ 5/a\ 6 S i1 i2) >\ 5a href="cic:/matita/tutorial/chapter9/move_plus.def(7)"\ 6move_plus\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_plus_w.def(8)"\ 6sem_plus_w\ 5/a\ 6
  97    @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6[|@\ 5a href="cic:/matita/tutorial/chapter8/sem_oplus.def(9)"\ 6sem_oplus\ 5/a\ 6]
  98    @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6[|@\ 5a href="cic:/matita/basics/logic/iff_or_l.def(2)"\ 6iff_or_l\ 5/a\ 6 [|@HI2]| @\ 5a href="cic:/matita/basics/logic/iff_or_r.def(2)"\ 6iff_or_r\ 5/a\ 6 //]
  99   |#i1 #HI1 #w >\ 5a href="cic:/matita/tutorial/chapter9/move_star.def(7)"\ 6move_star\ 5/a\ 6
 100    @\ 5a href="cic:/matita/basics/logic/iff_trans.def(2)"\ 6iff_trans\ 5/a\ 6[|@\ 5a href="cic:/matita/tutorial/chapter8/sem_ostar.def(13)"\ 6sem_ostar\ 5/a\ 6] >\ 5a href="cic:/matita/tutorial/chapter9/same_kernel.def(8)"\ 6same_kernel\ 5/a\ 6 >\ 5a href="cic:/matita/tutorial/chapter7/sem_star_w.def(8)"\ 6sem_star_w\ 5/a\ 6
 101    @\ 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/chapter6/deriv_middot.def(5)"\ 6deriv_middot\ 5/a\ 6 //]
 102    @\ 5a href="cic:/matita/tutorial/chapter6/cat_ext_l.def(5)"\ 6cat_ext_l\ 5/a\ 6 @HI1
 103   ]
 104 qed.
 105
 106 (* The move operation is generalized to strings in the obvious way. *)
 107
 108 notation > "x ↦* E" non associative with precedence 60 for @{moves ? $x $E}.
 109
 110 let rec moves (S : DeqSet) w e on w : pre S ≝
 111  match w with
 112   [ nil ⇒ e
 113   | cons x w' ⇒ w' ↦* (move S x (\fst e))].
 114
 115 lemma moves_empty: ∀S:DeqSet.∀e:pre S.
 116   moves ? [ ] e = e.
 117 // qed.
 118
 119 lemma moves_cons: ∀S:DeqSet.∀a:S.∀w.∀e:pre S.
 120   moves ? (a::w)  e = moves ? w (move S a (\fst e)).
 121 // qed.
 122
 123 lemma moves_left : ∀S,a,w,e.
 124   moves S (w@[a]) e = move S a (\fst (moves S w e)).
 125 #S #a #w elim w // #x #tl #Hind #e >moves_cons >moves_cons //
 126 qed.
 127
 128 lemma not_epsilon_sem: ∀S:DeqSet.∀a:S.∀w: word S. ∀e:pre S.
 129   iff ((a::w) ∈ e) ((a::w) ∈ \fst e).
 130 #S #a #w * #i #b cases b normalize
 131   [% /2/ * // #H destruct |% normalize /2/]
 132 qed.
 133
 134 lemma same_kernel_moves: ∀S:DeqSet.∀w.∀e:pre S.
 135   |\fst (moves ? w e)| = |\fst e|.
 136 #S #w elim w //
 137 qed.
 138
 139 theorem decidable_sem: ∀S:DeqSet.∀w: word S. ∀e:pre S.
 140    (\snd (moves ? w e) = true) ↔ \sem{e} w.
 141 #S #w elim w
 142  [* #i #b >moves_empty cases b % /2/
 143  |#a #w1 #Hind #e >moves_cons
 144   @iff_trans [||@iff_sym @not_epsilon_sem]
 145   @iff_trans [||@move_ok] @Hind
 146  ]
 147 qed.
 148
 149 (* It is now clear that we can build a DFA D_e for e by taking pre as states,
 150 and move as transition function; the initial state is •(e) and a state 〈i,b〉 is
 151 final if and only if b is true. The fact that states in D_e are finite is obvious:
 152 in fact, their cardinality is at most 2^{n+1} where n is the number of symbols in
 153 e. This is one of the advantages of pointed regular expressions w.r.t. derivatives,
 154 whose finite nature only holds after a suitable quotient.
 155
 156 Let us discuss a couple of examples.
 157
 158 \ 5b\ 6Example\ 5/b\ 6.
 159 Below is the DFA associated with the regular expression (ac+bc)*.
 160
 161 \ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/acUbc.gif" alt="DFA for (ac+bc)"/\ 6
 162
 163 The graphical description of the automaton is the traditional one, with nodes for
 164 states and labelled arcs for transitions. Unreachable states are not shown.
 165 Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
 166 only if b is true, we may just label nodes with the item.
 167 The automaton is not minimal: it is easy to see that the two states corresponding to
 168 the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
 169 that they define the same language!). In fact, an important property of pres e is that
 170 each state has a clear semantics, given in terms of the specification e and not of the
 171 behaviour of the automaton. As a consequence, the construction of the automaton is not
 172 only direct, but also extremely intuitive and locally verifiable.
 173
 174 Let us consider a more complex case.
 175
 176 \ 5b\ 6Example\ 5/b\ 6.
 177 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 178
 179 \ 5img src="http://www.cs.unibo.it/~asperti/FIGURES/automaton.gif" alt="DFA for (a+ϵ)(b*a + b)b"/\ 6
 180
 181 Remarkably, this DFA is minimal, testifying the small number of states produced by our
 182 technique (the pair ofstates 6-8 and 7-9 differ for the fact that 6 and 7
 183 are final, while 8 and 9 are not).
 184 *)
 185
 186 (*
 187 \ 5h2\ 6Move to pit\ 5/h2\ 6.
 188
 189 We conclude this chapter with a few properties of the move opertions in relation
 190 with the pit state. *).
 191
 192 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
 193
 194 (* The following function compute if a symbol in S occurs in a given
 195 item i *).
 196
 197 let rec occur (S: DeqSet) (i: re S) on i ≝
 198   match i with
 199   [ z ⇒ [ ]
 200   | e ⇒ [ ]
 201   | s y ⇒ [y]
 202   | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 203   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 204   | k e ⇒ occur S e].
 205
 206 (* If a symbol a does not occur in i, then move(i,a) gets to the
 207 pit state. *).
 208
 209 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
 210   move S a i  = pit_pre S i.
 211 #S #a #i elim i //
 212   [#x normalize cases (a==x) normalize // #H @False_ind /2/
 213   |#i1 #i2 #Hind1 #Hind2 #H >move_cat
 214    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 215    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 216   |#i1 #i2 #Hind1 #Hind2 #H >move_plus
 217    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 218    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 219   |#i #Hind #H >move_star >Hind //
 220   ]
 221 qed.
 222
 223 (* We cannot escape form the pit state. *).
 224
 225 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
 226 #S #a #i elim i //
 227   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
 228   |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
 229   |#i #Hind >move_star >Hind //
 230   ]
 231 qed.
 232
 233 lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
 234 #S #w #i elim w //
 235 qed.
 236
 237 (* If any character in w does not occur in i, then moves(i,w) gets
 238 to the pit state. *).
 239
 240 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
 241  moves S w e = pit_pre S (\fst e).
 242 #S #w elim w
 243   [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
 244   |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
 245     [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
 246      @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
 247       [#H2 >(\P H2) // |#H2 @H1 //]
 248     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
 249     ]
 250   ]
 251 qed.