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 Example. 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 Below is the DFA associated with the regular expression (ac+bc)*.
 158
 159 \includegraphics[width=.8\textwidth]{acUbc.pdf}
 160 \caption{DFA for $(ac+bc)^*$\label{acUbc}}
 161
 162 The graphical description of the automaton is the traditional one, with nodes for
 163 states and labelled arcs for transitions. Unreachable states are not shown.
 164 Final states are emphasized by a double circle: since a state 〈e,b〉 is final if and
 165 only if b is true, we may just label nodes with the item.
 166 The automaton is not minimal: it is easy to see that the two states corresponding to
 167 the items (a•c +bc)* and (ac+b•c)* are equivalent (a way to prove it is to observe
 168 that they define the same language!). In fact, an important property of pres e is that
 169 each state has a clear semantics, given in terms of the specification e and not of the
 170 behaviour of the automaton. As a consequence, the construction of the automaton is not
 171 only direct, but also extremely intuitive and locally verifiable.
 172
 173 Let us consider a more complex case.
 174 Starting form the regular expression (a+ϵ)(b*a + b)b, we obtain the following automaton.
 175
 176 \includegraphics[width=.8\textwidth]{automaton.pdf}
 177 \caption{DFA for $(a+\epsilon)(b^*a + b)b$\label{automaton}}
 178
 179 Remarkably, this DFA is minimal, testifying the small number of states produced by our
 180 technique (the pair ofstates $6-8$ and $7-9$ differ for the fact that $6$ and $7$
 181 are final, while $8$ and $9$ are not).
 182 *)
 183
 184 (************************ pit state ***************************)
 185 definition pit_pre ≝ λS.λi.〈blank S (|i|), false〉.
 186
 187 let rec occur (S: DeqSet) (i: re S) on i ≝
 188   match i with
 189   [ z ⇒ [ ]
 190   | e ⇒ [ ]
 191   | s y ⇒ [y]
 192   | o e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 193   | c e1 e2 ⇒ unique_append ? (occur S e1) (occur S e2)
 194   | k e ⇒ occur S e].
 195
 196 lemma not_occur_to_pit: ∀S,a.∀i:pitem S. memb S a (occur S (|i|)) ≠ true →
 197   move S a i  = pit_pre S i.
 198 #S #a #i elim i //
 199   [#x normalize cases (a==x) normalize // #H @False_ind /2/
 200   |#i1 #i2 #Hind1 #Hind2 #H >move_cat
 201    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 202    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 203   |#i1 #i2 #Hind1 #Hind2 #H >move_plus
 204    >Hind1 [2:@(not_to_not … H) #H1 @sublist_unique_append_l1 //]
 205    >Hind2 [2:@(not_to_not … H) #H1 @sublist_unique_append_l2 //] //
 206   |#i #Hind #H >move_star >Hind //
 207   ]
 208 qed.
 209
 210 lemma move_pit: ∀S,a,i. move S a (\fst (pit_pre S i)) = pit_pre S i.
 211 #S #a #i elim i //
 212   [#i1 #i2 #Hind1 #Hind2 >move_cat >Hind1 >Hind2 //
 213   |#i1 #i2 #Hind1 #Hind2 >move_plus >Hind1 >Hind2 //
 214   |#i #Hind >move_star >Hind //
 215   ]
 216 qed.
 217
 218 lemma moves_pit: ∀S,w,i. moves S w (pit_pre S i) = pit_pre S i.
 219 #S #w #i elim w //
 220 qed.
 221
 222 lemma to_pit: ∀S,w,e. ¬ sublist S w (occur S (|\fst e|)) →
 223  moves S w e = pit_pre S (\fst e).
 224 #S #w elim w
 225   [#e * #H @False_ind @H normalize #a #abs @False_ind /2/
 226   |#a #tl #Hind #e #H cases (true_or_false (memb S a (occur S (|\fst e|))))
 227     [#Htrue >moves_cons whd in ⊢ (???%); <(same_kernel … a)
 228      @Hind >same_kernel @(not_to_not … H) #H1 #b #memb cases (orb_true_l … memb)
 229       [#H2 >(\P H2) // |#H2 @H1 //]
 230     |#Hfalse >moves_cons >not_occur_to_pit // >Hfalse /2/
 231     ]
 232   ]
 233 qed.