matita/matita/lib/turing/multi_to_mono.ma

   1 include "turing/basic_machines.ma".
   2 include "turing/if_machine.ma".
   3 include "basics/vector_finset.ma".
   4 include "turing/auxiliary_machines1.ma".
   5
   6 (* a multi_sig characheter is composed by n+1 sub-characters: n for each tape
   7 of a multitape machine, and an additional one to mark the position of the head.
   8 We extend the tape alphabet with two new symbols true and false.
   9 false is used to pad shorter tapes, and true to mark the head of the tape *)
  10
  11 definition sig_ext ≝ λsig. FinSum FinBool sig.
  12 definition blank : ∀sig.sig_ext sig ≝ λsig. inl … false.
  13 definition head : ∀sig.sig_ext sig ≝ λsig. inl … true.
  14
  15 definition multi_sig ≝ λsig:FinSet.λn.FinVector (sig_ext sig) n.
  16
  17 let rec all_blank sig n on n : multi_sig sig n ≝
  18   match n with
  19   [ O ⇒ Vector_of_list ? []
  20   | S m ⇒ vec_cons ? (blank ?) m (all_blank sig m)
  21   ].
  22
  23 lemma blank_all_blank: ∀sig,n,i. i ≤ n →
  24   nth i ? (vec … (all_blank sig n)) (blank sig) = blank ?.
  25 #sig #n elim n normalize
  26   [#i #lei0 @(le_n_O_elim … lei0) normalize //
  27   |#m #Hind #i cases i // #j #lej @Hind @le_S_S_to_le //
  28   ]
  29 qed.
  30
  31 lemma all_blank_n: ∀sig,n.
  32   nth n ? (vec … (all_blank sig n)) (blank sig) = blank ?.
  33 #sig #n @blank_all_blank //
  34 qed.
  35
  36
  37 (* a machine that moves the i trace r: we reach the left margin of the i-trace
  38 and make a (shifted) copy of the old tape up to the end of the right margin of
  39 the i-trace. Then come back to the origin. *)
  40
  41 (* definition move_r_i *)
  42
  43 (* move_tape_i_step:
  44    we cycle on normal chars *)
  45 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
  46   change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
  47
  48 (* vec is a coercion. Why should I insert it? *)
  49 definition mti_step ≝ λsig:FinSet.λn,i.
  50   ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
  51      (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
  52      (nop ?) tc_true.
  53
  54 definition Rmti_step_true ≝
  55 λsig,n,i,t1,t2.
  56   ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
  57     ((∃ls,a,rs.
  58        t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
  59        t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
  60      (∃ls.
  61        t1 = midtape ? ls b [] ∧
  62        t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
  63
  64 (* 〈combf0,all_blank sig n〉 *)
  65 definition Rmti_step_false ≝
  66   λsig,n,i,t1,t2.
  67     (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
  68      (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
  69
  70 lemma sem_mti_step :
  71   ∀sig,n,i.
  72   mti_step sig n i  ⊨
  73     [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
  74 #sig #n #i
  75 @(acc_sem_if_app (multi_sig sig n) ??????????
  76      (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
  77      (sem_nop (multi_sig sig n)))
  78   [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
  79    #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
  80    #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
  81     [@(\Pf (injective_notb … )) @ctest]
  82    generalize in match Hintape; -Hintape cases rs
  83     [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
  84     |#a #rs1 #Hintape %1
  85      @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
  86      @Hout2 >Htapea @Hintape
  87     ]
  88   |#intape #outtape #tapea whd in ⊢ (%→%→%);
  89    * #Htest #tapea #outtape
  90    % // #ls #b #rs
  91    #intape lapply (Htest b ?) [>intape //] -Htest #Htest
  92    lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
  93   ]
  94 qed.
  95
  96 (* move tape i machine *)
  97 definition mti ≝
  98   λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
  99
 100 (* v2 is obtained from v1 shifting left the i-th trace *)
 101 definition shift_l ≝ λsig,n,i,v1,v2.  (* multi_sig sig n*)
 102   |v1| = |v2| ∧ ∀j. S j < |v1| →
 103     nth j ? v2 (all_blank sig n) =
 104       change_vec ? n (nth j ? v1 (all_blank sig n))
 105         (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
 106
 107 axiom daemon: ∀P:Prop.P.
 108
 109 definition R_mti ≝
 110   λsig,n,i,t1,t2.
 111     (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
 112     (∀a,ls,rs.
 113       t1 = midtape (multi_sig sig n) ls a rs →
 114       (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
 115       ((∃rs1,b,rs2,rss.
 116         rs = rs1@b::rs2 ∧
 117         nth i ? (vec … b) (blank ?) = (blank ?) ∧
 118         (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 119         shift_l sig n i (a::rs1) rss ∧
 120         t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
 121       (∃b,rss.
 122         (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 123         shift_l sig n i (a::rs) (rss@[b]) ∧
 124         t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n))
 125          ((reverse ? rss)@ls)))).
 126
 127 lemma sem_mti:
 128   ∀sig,n,i.
 129   WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
 130 #sig #n #i #inc #j #outc #Hloop
 131 lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
 132 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 133 [ whd in ⊢ (% → ?); * #H1 #H2 %
 134   [#a #rs #Htape1 @H2
 135   |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
 136   ]
 137 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 138   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
 139   * #IH1 #IH2 %
 140   [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
 141     [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
 142     |* #ls0 * >Htapeb #H destruct (H)
 143     ]
 144   |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
 145   [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
 146    %2 cases (IH2 … Htapec)
 147     [(* case a = None *)
 148      * #testa #Hout %1
 149      %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
 150       [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
 151         |@daemon]
 152       |>Hout >reverse_single @Htapec
 153       ]
 154     |*
 155       [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
 156         %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
 157         #H1 #H2 #H3 #H4 #H5
 158         %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
 159         %[%[%[%[>H1 //|@H2]
 160             |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
 161           |@daemon]
 162         |>H5 >reverse_cons >associative_append //
 163         ]
 164       | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
 165         %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
 166         %{b0} %{(shift_i sig n i b a::rss)}
 167         %[%[#x * [#eqxb >eqxb @btest|@H1]
 168            |@daemon]
 169         |>H3 >reverse_cons >associative_append //
 170         ]
 171       ]
 172     ]
 173   |(* b \= None but the left tape is empty *)
 174    * #ls0 * >Htapeb #H destruct (H) #Htapec
 175    %2 %2 %{b} %{[ ]}
 176    %[%[#x * [#eqxb >eqxb @btest|@False_ind]
 177       |@daemon (*shift of  dingle char OK *)]
 178     |>(IH1 … Htapec) >Htapec //
 179     ]
 180   ]
 181 qed.
 182
 183 lemma WF_mti_niltape:
 184   ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
 185 #sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 186   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 187 qed.
 188
 189 lemma WF_mti_rightof:
 190   ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
 191 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 192   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 193 qed.
 194
 195 lemma WF_mti_leftof:
 196   ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
 197 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 198   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 199 qed.
 200
 201 lemma terminate_mti:
 202   ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
 203 #sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
 204 cases t // #ls #c #rs lapply c -c lapply ls -ls  elim rs
 205   [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 206     [* #ls1 * #a * #rs1 * #H destruct
 207     |* #ls1 * #H destruct #Ht1 >Ht1 //
 208     ]
 209   |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 210     [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
 211     |* #ls1 *  #H destruct
 212     ]
 213   ]
 214 qed.
 215
 216 lemma ssem_mti: ∀sig,n,i.
 217   Realize ? (mti sig n i) (R_mti sig n i).
 218 /2/ qed.
 219
 220 (******************************************************************************)
 221 (* mtiL: complete move L for tape i. We reaching the left border of trace i,  *)
 222 (* add a blank if there is no more tape, then move the i-trace and finally    *)
 223 (* come back to the head position.                                            *)
 224 (******************************************************************************)
 225
 226 definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
 227   ¬(nth i ? (vec … c) (blank ?))==blank ?.
 228
 229 definition no_head ≝ λsig,n.λc:multi_sig sig n.
 230   ¬((nth n ? (vec … c) (blank ?))==head ?).
 231
 232 definition mtiL ≝ λsig,n,i.
 233    move_until ? L (no_blank sig n i) ·
 234    extend ? (all_blank sig n) ·
 235    ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
 236    mti sig n i ·
 237    extend ? (all_blank sig n) ·
 238    move_until ? L (no_head sig n).
 239
 240 let rec to_blank sig n i l on l ≝
 241   match l with
 242   [ nil ⇒  [ ]
 243   | cons a tl ⇒
 244       let ai ≝ nth i ? (vec … n a) (blank sig) in
 245       if ai == blank ? then [ ] else ai::(to_blank sig n i tl)].
 246
 247 lemma to_blank_cons_b : ∀sig,n,i,a,l.
 248   nth i ? (vec … n a) (blank sig) = blank ? →
 249   to_blank sig n i (a::l) = [ ].
 250 #sig #n #i #a #l #H whd in match (to_blank ????);
 251 >(\b H) //
 252 qed.
 253
 254 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
 255   nth i ? (vec … n a) (blank sig) ≠ blank ? →
 256   to_blank sig n i (a::l) =
 257     nth i ? (vec … n a) (blank sig)::(to_blank sig n i l).
 258 #sig #n #i #a #l #H whd in match (to_blank ????);
 259 >(\bf H) //
 260 qed.
 261
 262 (******************************* move_to_blank_L ******************************)
 263 (* we compose machines together to reduce the number of output cases, and
 264    improve semantics *)
 265
 266 definition move_to_blank_L ≝ λsig,n,i.
 267   (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
 268
 269 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
 270 (current ? t1 = None ? →
 271   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
 272 ∀ls,a,rs.t1 = midtape ? ls a rs →
 273   ((no_blank sig n i a = false) ∧ t2 = t1) ∨
 274   (∃b,ls1,ls2.
 275     (no_blank sig n i b = false) ∧
 276     (∀j.j ≤n → to_blank ?? j (ls1@b::ls2) = to_blank ?? j ls) ∧
 277     t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)).
 278
 279 theorem sem_move_to_blank_L: ∀sig,n,i.
 280   move_to_blank_L sig n i  ⊨ R_move_to_blank_L sig n i.
 281 #sig #n #i
 282 @(sem_seq_app ??????
 283   (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
 284 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
 285   [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
 286   |#ls #a #rs #Htin -Ht1a cases (Ht1b … Htin)
 287     [* #Hnb #Ht1 -Ht1b -Ht2a >Ht1 in Ht2b; >Htin #H %1
 288      % [//|@H normalize % #H1 destruct (H1)]
 289     |*
 290     [(* we find the blank *)
 291      * #ls1 * #b * #ls2 * * * #H1 #H2 #H3 #H4 %2
 292      %{b} %{ls1} %{ls2}
 293      %[%[@H2|>H1 //]
 294       |-Ht1b -Ht2a >H4 in Ht2b; #H5 @H5
 295        % normalize #H6 destruct (H6)
 296       ]
 297     |* #b * #lss * * #H1 #H2 #H3 %2
 298      %{(all_blank …)} %{ls} %{[ ]}
 299      %[%[whd in match (no_blank ????); >blank_all_blank // @daemon
 300         |@daemon (* make a lemma *)]
 301       |-Ht1b -Ht2b >H3 in Ht2a;
 302        whd in match (left ??); whd in match (right ??); #H4
 303        >H2 >reverse_append >reverse_single @H4 normalize //
 304       ]
 305     ]
 306   ]
 307 qed.
 308
 309 (******************************************************************************)
 310
 311 definition shift_i_L ≝ λsig,n,i.
 312    ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
 313    mti sig n i ·
 314    extend ? (all_blank sig n).
 315
 316 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
 317   (* ∀b:multi_sig sig n.∀ls.
 318     (t1 = midtape ? ls b [ ] →
 319      t2 = midtape (multi_sig sig n)
 320       ((shift_i sig n i b (all_blank sig n))::ls) (all_blank sig n) [ ]) ∧ *)
 321     (∀a,ls,rs.
 322       t1 = midtape ? ls a rs  →
 323       ((∃rs1,b,rs2,rss.
 324         rs = rs1@b::rs2 ∧
 325         nth i ? (vec … b) (blank ?) = (blank ?) ∧
 326         (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 327         shift_l sig n i (a::rs1) rss ∧
 328         t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
 329       (∃b,rss.
 330         (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 331         shift_l sig n i (a::rs) (rss@[b]) ∧
 332         t2 = midtape (multi_sig sig n)
 333           ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
 334
 335 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i  ⊨ R_shift_i_L sig n i.
 336 #sig #n #i
 337 @(sem_seq_app ??????
 338   (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
 339    (sem_seq ????? (ssem_mti sig n i)
 340     (sem_extend ? (all_blank sig n))))
 341 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
 342 (* #b #ls %
 343   [#Htin lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 344    lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 345    >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout // *)
 346 #a #ls #rs cases rs
 347   [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
 348    %[%[#x @False_ind | @daemon]
 349     |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 350      lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 351      >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout //
 352     ]
 353   |#a1 #rs1 #Htin
 354    lapply (Ht1b … Htin) -Ht1a -Ht1b #Ht1
 355    lapply (Ht2b … Ht1) -Ht2a -Ht2b *
 356     [(* a1 is blank *) * #H1 #H2 %1
 357      %{[ ]} %{a1} %{rs1} %{[shift_i sig n i a a1]}
 358      %[%[%[%[// |//] |#x @False_ind] | @daemon]
 359       |>Htout2 [>H2 >reverse_single @Ht1 |>H2 >Ht1 normalize % #H destruct (H)]
 360       ]
 361     |*
 362     [* #rs10 * #b * #rs2 * #rss * * * * #H1 #H2 #H3 #H4
 363      #Ht2 %1
 364      %{(a1::rs10)} %{b} %{rs2} %{(shift_i sig n i a a1::rss)}
 365      %[%[%[%[>H1 //|//] |@H3] |@daemon ]
 366       |>reverse_cons >associative_append
 367        >H2 in Htout2; #Htout >Htout [@Ht2| >Ht2 normalize % #H destruct (H)]
 368       ]
 369     |* #b * #rss * * #H1 #H2
 370      #Ht2 %2
 371      %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
 372      %[%[@H1 |@daemon ]
 373       |>Ht2 in Htout1; #Htout >Htout //
 374        whd in match (left ??); whd in match (right ??);
 375        >reverse_append >reverse_single >associative_append  >reverse_cons
 376        >associative_append //
 377        ]
 378      ]
 379    ]
 380  ]
 381 qed.
 382
 383
 384 definition Rmtil ≝ λsig,n,i,t1,t2.
 385   ∀ls,a,rs.
 386    t1 = midtape ? ls a rs →
 387    nth n ? (vec … a) (blank ?) = head ? →
 388    (∀x.mem ? x ls → no_head sig n x = true) →
 389    (∀x.mem ? x rs → no_head sig n x = true) →
 390    (∃ls1,a1,rs1.
 391      t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
 392      (∀j. j ≤ n → j ≠ i → to_blank ? n j ls1 = to_blank ? n j ls) ∧
 393      (∀j. j ≤ n → j ≠ i → to_blank ? n j rs1 = to_blank ? n j rs) ∧
 394      (nth i ? (vec … a) (blank ?) = blank ? → ls1 = ls) ∧
 395      (nth i ? (vec … a) (blank ?) ≠ blank ? → to_blank ? n i ls1 = nth i ? (vec … a) (blank ?)::to_blank ? n i ls) ∧
 396      (to_blank ? n i (a1::rs1)) = to_blank ? n i rs).
 397
 398 theorem sem_Rmtil: ∀sig,n,i. mtiL sig n i  ⊨ Rmtil sig n i.
 399 #sig #n #i
 400 @(sem_seq_app ??????
 401   (ssem_move_until_L ? (no_blank sig n i))
 402    (sem_seq ????? (sem_extend ? (all_blank sig n))
 403     (sem_seq ????? (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
 404      (sem_seq ????? (ssem_mti sig n i)
 405       (sem_seq ????? (sem_extend ? (all_blank sig n))
 406        (ssem_move_until_L ? (no_head sig n)))))))
 407 #tin #tout * #t1 * * #_ #Ht1 * #t2 * * #Ht2a #Ht2b * #t3 * * #Ht3a #Ht3b
 408 * #t4 * * #Ht4a #Ht4b * #t5 * * #Ht5a #Ht5b * #t6 #Htout
 409 (* we start looking into Rmitl *)
 410 #ls #a #rs #Htin (* tin is a midtape *)
 411 #Hhead #Hnohead_ls #Hnohead_rs
 412 cases (Ht1 … Htin) -Ht1
 413   [(* the current character on trace i is blank *)
 414    -Ht2a * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2b;
 415    #Ht2b lapply (Ht2b ?) [% normalize #H destruct] -Ht2b -Ht1 -Ht1a
 416    lapply Hnohead_rs -Hnohead_rs
 417    (* by cases on rs *) cases rs
 418     [#_ (* rs is empty *) #Ht2 -Ht3b lapply (Ht3a … Ht2)
 419      #Ht3 -Ht4b lapply (Ht4a … Ht3) -Ht4a #Ht4 -Ht5b
 420      >Ht4 in Ht5a; >Ht3 #Ht5a lapply (Ht5a (refl … )) -Ht5a #Ht5
 421      cases (Htout … Ht5) -Htout
 422       [(* the current symbol on trace n is the head: this is absurd *)
 423        * whd in ⊢ (??%?→?); >all_blank_n whd in ⊢ (??%?→?); #H destruct (H)
 424       |*
 425       [(* we return to the head *)
 426        * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
 427        #H1 #H2 #H3
 428        (* ls1 must be empty *)
 429        cut (ls1=[])
 430         [lapply H3 lapply H1 -H3 -H1 cases ls1 // #c #ls3
 431          whd in ⊢ (???%→?); #H1 destruct (H1)
 432          >blank_all_blank [|@daemon] #H @False_ind
 433          lapply (H … (change_vec (sig_ext sig) n a (blank sig) i) ?)
 434           [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 435            >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
 436        #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
 437        >reverse_single >blank_all_blank [|@daemon]
 438        whd in match (right ??) ; >append_nil #Htout
 439        %{ls2} %{(change_vec (sig_ext sig) n a (blank sig) i)} %{[all_blank sig n]}
 440        %[%[%[%[%[//|//]|@daemon]|//] |(*absurd*)@daemon]
 441         |normalize >nth_change_vec // @daemon]
 442       |(* we do not find the head: this is absurd *)
 443        * #b * #lss * * whd in match (left ??); #HF @False_ind
 444        lapply (HF … (shift_i sig n i a (all_blank sig n)) ?) [%2 %1 //]
 445        whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 446        >Hhead whd in ⊢ (??%?→?); #H destruct (H)
 447       ]
 448       ]
 449     |(* rs = c::rs1 *)
 450      #c #rs1 #Hnohead_rs #Ht2 -Ht3a lapply (Ht3b … Ht2) -Ht3b
 451      #Ht3 -Ht4a lapply (Ht4b … Ht3) -Ht4b *
 452       [(* the first character is blank *) *
 453        #Hblank #Ht4 -Ht5a >Ht4 in Ht5b; >Ht3
 454        normalize in ⊢ ((%→?)→?); #Ht5 lapply (Ht5 ?) [% #H destruct (H)]
 455        -Ht2 -Ht3 -Ht4 -Ht5 #Ht5 cases (Htout … Ht5) -Htout
 456         [(* the current symbol on trace n is the head: this is absurd *)
 457          * >Hnohead_rs [#H destruct (H) |%1 //]
 458         |*
 459         [(* we return to the head *)
 460          * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
 461          #H1 #H2 #H3
 462          (* ls1 must be empty *)
 463          cut (ls1=[])
 464           [lapply H3 lapply H1 -H3 -H1 cases ls1 // #x #ls3
 465            whd in ⊢ (???%→?); #H1 destruct (H1) #H @False_ind
 466            lapply (H (change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i) ?)
 467             [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 468              >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
 469          #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
 470          >reverse_single #Htout
 471          %{ls2} %{(change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i)}
 472          %{(c::rs1)}
 473          %[%[%[%[%[@Htout|//]|//]|//] |(*absurd*)@daemon]
 474           |>to_blank_cons_b
 475              [>(to_blank_cons_b … Hblank) //| >nth_change_vec [@Hblank |@daemon]]
 476           ]
 477         |(* we do not find the head: this is absurd *)
 478          * #b * #lss * * #HF @False_ind
 479          lapply (HF … (shift_i sig n i a c) ?) [%2 %1 //]
 480          whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 481          >Hhead whd in ⊢ (??%?→?); #H destruct (H)
 482         ]
 483       ]
 484     |
 485
 486   (* end of the first case !! *)
 487
 488
 489
 490    #Ht2
 491
 492
 493
 494