matita/matita/lib/turing/multi_to_mono/multi_to_mono.ma

   1 include "turing/basic_machines.ma".
   2 include "turing/if_machine.ma".
   3 include "turing/auxiliary_machines1.ma".
   4 include "turing/multi_to_mono/trace_alphabet.ma".
   5
   6 (* a machine that moves the i trace r: we reach the left margin of the i-trace
   7 and make a (shifted) copy of the old tape up to the end of the right margin of
   8 the i-trace. Then come back to the origin. *)
   9
  10 definition shift_i ≝ λsig,n,i.λa,b:Vector (sig_ext sig) n.
  11   change_vec (sig_ext sig) n a (nth i ? b (blank ?)) i.
  12
  13 (* vec is a coercion. Why should I insert it? *)
  14 definition mti_step ≝ λsig:FinSet.λn,i.
  15   ifTM (multi_sig sig n) (test_char ? (λc:multi_sig sig n.¬(nth i ? (vec … c) (blank ?))==blank ?))
  16      (single_finalTM … (ncombf_r (multi_sig sig n) (shift_i sig n i) (all_blank sig n)))
  17      (nop ?) tc_true.
  18
  19 definition Rmti_step_true ≝
  20 λsig,n,i,t1,t2.
  21   ∃b:multi_sig sig n. (nth i ? (vec … b) (blank ?) ≠ blank ?) ∧
  22     ((∃ls,a,rs.
  23        t1 = midtape (multi_sig sig n) ls b (a::rs) ∧
  24        t2 = midtape (multi_sig sig n) ((shift_i sig n i b a)::ls) a rs) ∨
  25      (∃ls.
  26        t1 = midtape ? ls b [] ∧
  27        t2 = rightof ? (shift_i sig n i b (all_blank sig n)) ls)).
  28
  29 (* 〈combf0,all_blank sig n〉 *)
  30 definition Rmti_step_false ≝
  31   λsig,n,i,t1,t2.
  32     (∀ls,b,rs. t1 = midtape (multi_sig sig n) ls b rs →
  33      (nth i ? (vec … b) (blank ?) = blank ?)) ∧ t2 = t1.
  34
  35 lemma sem_mti_step :
  36   ∀sig,n,i.
  37   mti_step sig n i  ⊨
  38     [inr … (inl … (inr … start_nop)): Rmti_step_true sig n i, Rmti_step_false sig n i].
  39 #sig #n #i
  40 @(acc_sem_if_app (multi_sig sig n) ??????????
  41      (sem_test_char …) (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
  42      (sem_nop (multi_sig sig n)))
  43   [#intape #outtape #tapea whd in ⊢ (%→%→%); * * #c *
  44    #Hcur cases (current_to_midtape … Hcur) #ls * #rs #Hintape
  45    #ctest #Htapea * #Hout1 #Hout2 @(ex_intro … c) %
  46     [@(\Pf (injective_notb … )) @ctest]
  47    generalize in match Hintape; -Hintape cases rs
  48     [#Hintape %2 @(ex_intro …ls) % // @Hout1 >Htapea @Hintape
  49     |#a #rs1 #Hintape %1
  50      @(ex_intro … ls) @(ex_intro … a) @(ex_intro … rs1) % //
  51      @Hout2 >Htapea @Hintape
  52     ]
  53   |#intape #outtape #tapea whd in ⊢ (%→%→%);
  54    * #Htest #tapea #outtape
  55    % // #ls #b #rs
  56    #intape lapply (Htest b ?) [>intape //] -Htest #Htest
  57    lapply (injective_notb ? true Htest) -Htest #Htest @(\P Htest)
  58   ]
  59 qed.
  60
  61 (* move tape i machine *)
  62 definition mti ≝
  63   λsig,n,i.whileTM (multi_sig sig n) (mti_step sig n i) (inr … (inl … (inr … start_nop))).
  64
  65 (* v2 is obtained from v1 shifting left the i-th trace *)
  66 definition shift_l ≝ λsig,n,i,v1,v2.  (* multi_sig sig n*)
  67   |v1| = |v2| ∧
  68   ∀j.nth j ? v2 (all_blank sig n) =
  69       change_vec ? n (nth j ? v1 (all_blank sig n))
  70         (nth i ? (vec … (nth (S j) ? v1 (all_blank sig n))) (blank ?)) i.
  71
  72 lemma trace_shift: ∀sig,n,i,v1,v2. i < n → 0 < |v1| →
  73   shift_l sig n i v1 v2 → trace ? n i v2 = tail ? (trace ? n i v1)@[blank sig].
  74 #sig #n #i #v1 #v2 #lein #Hlen * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
  75   [>length_trace <Hlen1 generalize in match Hlen; cases v1
  76     [normalize #H @(le_n_O_elim … H) //
  77     |#b #tl #_ normalize >length_append >length_trace normalize //
  78     ]
  79   |#j >nth_trace >Hnth >nth_change_vec // >tail_trace
  80    cut (trace ? n i [all_blank sig n] = [blank sig])
  81      [normalize >blank_all_blank //]
  82    #Hcut <Hcut <trace_append >nth_trace
  83    <nth_extended //
  84   ]
  85 qed.
  86
  87 lemma trace_shift_neq: ∀sig,n,i,j,v1,v2. i < n → 0 < |v1| → i ≠ j →
  88   shift_l sig n i v1 v2 → trace ? n j v2 = trace ? n j v1.
  89 #sig #n #i #j #v1 #v2 #lein #Hlen #Hneq * #Hlen1 #Hnth @(nth_to_eq … (blank ?))
  90   [>length_trace >length_trace @sym_eq @Hlen1
  91   |#k >nth_trace >Hnth >nth_change_vec_neq // >nth_trace //
  92   ]
  93 qed.
  94
  95 axiom daemon: ∀P:Prop.P.
  96
  97 definition R_mti ≝
  98   λsig,n,i,t1,t2.
  99     (∀a,rs. t1 = rightof ? a rs → t2 = t1) ∧
 100     (∀a,ls,rs.
 101       t1 = midtape (multi_sig sig n) ls a rs →
 102       (nth i ? (vec … a) (blank ?) = blank ? ∧ t2 = t1) ∨
 103       ((∃rs1,b,rs2,rss.
 104         rs = rs1@b::rs2 ∧
 105         nth i ? (vec … b) (blank ?) = (blank ?) ∧
 106         (∀x. mem ? x (a::rs1) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 107         shift_l sig n i (a::rs1) rss ∧
 108         t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b rs2) ∨
 109       (∃b,rss.
 110         (∀x. mem ? x (a::rs) → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 111         shift_l sig n i (a::rs) (rss@[b]) ∧
 112         t2 = rightof (multi_sig sig n) (shift_i sig n i b (all_blank sig n))
 113          ((reverse ? rss)@ls)))).
 114
 115 lemma sem_mti:
 116   ∀sig,n,i.
 117   WRealize (multi_sig sig n) (mti sig n i) (R_mti sig n i).
 118 #sig #n #i #inc #j #outc #Hloop
 119 lapply (sem_while … (sem_mti_step sig n i) inc j outc Hloop) [%]
 120 -Hloop * #t1 * #Hstar @(star_ind_l ??????? Hstar)
 121 [ whd in ⊢ (% → ?); * #H1 #H2 %
 122   [#a #rs #Htape1 @H2
 123   |#a #ls #rs #Htapea % % [@(H1 … Htapea) |@H2]
 124   ]
 125 | #tapeb #tapec #Hstar1 #HRtrue #IH #HRfalse
 126   lapply (IH HRfalse) -IH -HRfalse whd in ⊢ (%→%);
 127   * #IH1 #IH2 %
 128   [#b0 #ls #Htapeb cases Hstar1 #b * #_ *
 129     [* #ls0 * #a * #rs0 * >Htapeb #H destruct (H)
 130     |* #ls0 * >Htapeb #H destruct (H)
 131     ]
 132   |#b0 #ls #rs #Htapeb cases Hstar1 #b * #btest *
 133   [* #ls1 * #a * #rs1 * >Htapeb #H destruct (H) #Htapec
 134    %2 cases (IH2 … Htapec)
 135     [(* case a = None *)
 136      * #testa #Hout %1
 137      %{[ ]} %{a} %{rs1} %{[shift_i sig n i b a]} %
 138       [%[%[% // |#x #Hb >(mem_single ??? Hb) // ]
 139         |@daemon]
 140       |>Hout >reverse_single @Htapec
 141       ]
 142     |*
 143       [ (* case a \= None and exists b = None *) -IH1 -IH2 #IH
 144         %1 cases IH -IH #rs10 * #b0 * #rs2 * #rss * * * *
 145         #H1 #H2 #H3 #H4 #H5
 146         %{(a::rs10)} %{b0} %{rs2} %{(shift_i sig n i b a::rss)}
 147         %[%[%[%[>H1 //|@H2]
 148             |#x * [#eqxa >eqxa (*?? *) @daemon|@H3]]
 149           |@daemon]
 150         |>H5 >reverse_cons >associative_append //
 151         ]
 152       | (* case a \= None and we reach the end of the (full) tape *) -IH1 -IH2 #IH
 153         %2 cases IH -IH #b0 * #rss * * #H1 #H2 #H3
 154         %{b0} %{(shift_i sig n i b a::rss)}
 155         %[%[#x * [#eqxb >eqxb @btest|@H1]
 156            |@daemon]
 157         |>H3 >reverse_cons >associative_append //
 158         ]
 159       ]
 160     ]
 161   |(* b \= None but the left tape is empty *)
 162    * #ls0 * >Htapeb #H destruct (H) #Htapec
 163    %2 %2 %{b} %{[ ]}
 164    %[%[#x * [#eqxb >eqxb @btest|@False_ind]
 165       |@daemon (*shift of  dingle char OK *)]
 166     |>(IH1 … Htapec) >Htapec //
 167     ]
 168   ]
 169 qed.
 170
 171 lemma WF_mti_niltape:
 172   ∀sig,n,i. WF ? (inv ? (Rmti_step_true sig n i)) (niltape ?).
 173 #sig #n #i @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 174   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 175 qed.
 176
 177 lemma WF_mti_rightof:
 178   ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (rightof ? a ls).
 179 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 180   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 181 qed.
 182
 183 lemma WF_mti_leftof:
 184   ∀sig,n,i,a,ls. WF ? (inv ? (Rmti_step_true sig n i)) (leftof ? a ls).
 185 #sig #n #i #a #ls @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 186   [* #ls * #a * #rs * #H destruct|* #ls * #H destruct ]
 187 qed.
 188
 189 lemma terminate_mti:
 190   ∀sig,n,i.∀t. Terminate ? (mti sig n i) t.
 191 #sig #n #i #t @(terminate_while … (sem_mti_step sig n i)) [%]
 192 cases t // #ls #c #rs lapply c -c lapply ls -ls  elim rs
 193   [#ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 194     [* #ls1 * #a * #rs1 * #H destruct
 195     |* #ls1 * #H destruct #Ht1 >Ht1 //
 196     ]
 197   |#a #rs1 #Hind #ls #c @wf #t1 whd in ⊢ (%→?); * #b * #_ *
 198     [* #ls1 * #a2 * #rs2 * #H destruct (H) #Ht1 >Ht1 //
 199     |* #ls1 *  #H destruct
 200     ]
 201   ]
 202 qed.
 203
 204 lemma ssem_mti: ∀sig,n,i.
 205   Realize ? (mti sig n i) (R_mti sig n i).
 206 /2/ qed.
 207
 208 (******************************************************************************)
 209 (* mtiL: complete move L for tape i. We reaching the left border of trace i,  *)
 210 (* add a blank if there is no more tape, then move the i-trace and finally    *)
 211 (* come back to the head position.                                            *)
 212 (******************************************************************************)
 213
 214 definition no_blank ≝ λsig,n,i.λc:multi_sig sig n.
 215   ¬(nth i ? (vec … c) (blank ?))==blank ?.
 216
 217 definition no_head ≝ λsig,n.λc:multi_sig sig n.
 218   ¬((nth n ? (vec … c) (blank ?))==head ?).
 219
 220 let rec to_blank sig l on l ≝
 221   match l with
 222   [ nil ⇒  [ ]
 223   | cons a tl ⇒
 224       if a == blank sig then [ ] else a::(to_blank sig tl)].
 225
 226 definition to_blank_i ≝ λsig,n,i,l. to_blank ? (trace sig n i l).
 227
 228 lemma to_blank_i_def : ∀sig,n,i,l.
 229   to_blank_i sig n i l = to_blank ? (trace sig n i l).
 230 // qed.
 231 (*
 232   match l with
 233   [ nil ⇒  [ ]
 234   | cons a tl ⇒
 235       let ai ≝ nth i ? (vec … n a) (blank sig) in
 236       if ai == blank ? then [ ] else ai::(to_blank sig n i tl)]. *)
 237
 238 lemma to_blank_cons_b : ∀sig,n,i,a,l.
 239   nth i ? (vec … n a) (blank sig) = blank ? →
 240   to_blank_i sig n i (a::l) = [ ].
 241 #sig #n #i #a #l #H whd in match (to_blank_i ????);
 242 >(\b H) //
 243 qed.
 244
 245 lemma to_blank_cons_nb: ∀sig,n,i,a,l.
 246   nth i ? (vec … n a) (blank sig) ≠ blank ? →
 247   to_blank_i sig n i (a::l) =
 248     nth i ? (vec … n a) (blank sig)::(to_blank_i sig n i l).
 249 #sig #n #i #a #l #H whd in match (to_blank_i ????);
 250 >(\bf H) //
 251 qed.
 252
 253 axiom to_blank_hd : ∀sig,n,a,b,l1,l2.
 254   (∀i. i ≤ n → to_blank_i sig n i (a::l1) = to_blank_i sig n i (b::l2)) → a = b.
 255
 256 lemma to_blank_i_ext : ∀sig,n,i,l.
 257   to_blank_i sig n i l = to_blank_i sig n i (l@[all_blank …]).
 258 #sig #n #i #l elim l
 259   [@sym_eq @to_blank_cons_b @blank_all_blank
 260   |#a #tl #Hind whd in match (to_blank_i ????); >Hind <to_blank_i_def >Hind %
 261   ]
 262 qed.
 263
 264 lemma to_blank_hd_cons : ∀sig,n,i,l1,l2.
 265   to_blank_i sig n i (l1@l2) =
 266     to_blank_i … i (l1@(hd … l2 (all_blank …))::tail … l2).
 267 #sig #n #i #l1 #l2 cases l2
 268   [whd in match (hd ???); whd in match (tail ??); >append_nil @to_blank_i_ext
 269   |#a #tl %
 270   ]
 271 qed.
 272
 273 lemma to_blank_i_chop : ∀sig,n,i,a,l1,l2.
 274  (nth i ? (vec … a) (blank ?))= blank ? →
 275  to_blank_i sig n i (l1@a::l2) = to_blank_i sig n i l1.
 276 #sig #n #i #a #l1 elim l1
 277   [#l2 #H @to_blank_cons_b //
 278   |#x #tl #Hind #l2 #H whd in match (to_blank_i ????);
 279    >(Hind l2 H) <to_blank_i_def >(Hind l2 H) %
 280   ]
 281 qed.
 282
 283 (******************************* move_to_blank_L ******************************)
 284 (* we compose machines together to reduce the number of output cases, and
 285    improve semantics *)
 286
 287 definition move_to_blank_L ≝ λsig,n,i.
 288   (move_until ? L (no_blank sig n i)) · extend ? (all_blank sig n).
 289
 290 definition R_move_to_blank_L ≝ λsig,n,i,t1,t2.
 291 (current ? t1 = None ? →
 292   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
 293 ∀ls,a,rs.t1 = midtape ? ls a rs →
 294   ((no_blank sig n i a = false) ∧ t2 = t1) ∨
 295   (∃b,ls1,ls2.
 296     (no_blank sig n i b = false) ∧
 297     (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j ls) ∧
 298     t2 = midtape ? ls2 b ((reverse ? (a::ls1))@rs)).
 299
 300 definition R_move_to_blank_L_new ≝ λsig,n,i,t1,t2.
 301 (current ? t1 = None ? →
 302   t2 = midtape (multi_sig sig n) (left ? t1) (all_blank …) (right ? t1)) ∧
 303 ∀ls,a,rs.t1 = midtape ? ls a rs →
 304   (∃b,ls1,ls2.
 305     (no_blank sig n i b = false) ∧
 306     (hd ? (ls1@[b]) (all_blank …) = a) ∧ (* not implied by the next fact *)
 307     (∀j.j ≤n → to_blank_i ?? j (ls1@b::ls2) = to_blank_i ?? j (a::ls)) ∧
 308     t2 = midtape ? ls2 b ((reverse ? ls1)@rs)).
 309
 310 theorem sem_move_to_blank_L: ∀sig,n,i.
 311   move_to_blank_L sig n i  ⊨ R_move_to_blank_L sig n i.
 312 #sig #n #i
 313 @(sem_seq_app ??????
 314   (ssem_move_until_L ? (no_blank sig n i)) (sem_extend ? (all_blank sig n)))
 315 #tin #tout * #t1 * * #Ht1a #Ht1b * #Ht2a #Ht2b %
 316   [#Hcur >(Ht1a Hcur) in Ht2a; /2 by /
 317   |#ls #a #rs #Htin -Ht1a cases (Ht1b … Htin)
 318     [* #Hnb #Ht1 -Ht1b -Ht2a >Ht1 in Ht2b; >Htin #H %1
 319      % [//|@H normalize % #H1 destruct (H1)]
 320     |*
 321     [(* we find the blank *)
 322      * #ls1 * #b * #ls2 * * * #H1 #H2 #H3 #H4 %2
 323      %{b} %{ls1} %{ls2}
 324      %[%[@H2|>H1 //]
 325       |-Ht1b -Ht2a >H4 in Ht2b; #H5 @H5
 326        % normalize #H6 destruct (H6)
 327       ]
 328     |* #b * #lss * * #H1 #H2 #H3 %2
 329      %{(all_blank …)} %{ls} %{[ ]}
 330      %[%[whd in match (no_blank ????); >blank_all_blank // @daemon
 331         |@daemon (* make a lemma *)]
 332       |-Ht1b -Ht2b >H3 in Ht2a;
 333        whd in match (left ??); whd in match (right ??); #H4
 334        >H2 >reverse_append >reverse_single @H4 normalize //
 335       ]
 336     ]
 337   ]
 338 qed.
 339
 340 theorem sem_move_to_blank_L_new: ∀sig,n,i.
 341   move_to_blank_L sig n i  ⊨ R_move_to_blank_L_new sig n i.
 342 #sig #n #i
 343 @(Realize_to_Realize … (sem_move_to_blank_L sig n i))
 344 #t1 #t2 * #H1 #H2 % [@H1]
 345 #ls #a #rs #Ht1 lapply (H2 ls a rs Ht1) -H2 *
 346   [* #Ha #Ht2 >Ht2 %{a} %{[ ]} %{ls}
 347    %[%[%[@Ha| //]| normalize //] | @Ht1]
 348   |* #b * #ls1 * #ls2 * * * #Hblank #Ht2
 349    %{b} %{(a::ls1)} %{ls2}
 350    %[2:@Ht2|%[%[//|//]|
 351    #j #lejn whd in match (to_blank_i ????);
 352    whd in match (to_blank_i ???(a::ls));
 353    lapply (Hblank j lejn) whd in match (to_blank_i ????);
 354    whd in match (to_blank_i ???(a::ls)); #H >H %
 355   ]
 356 qed.
 357
 358 (******************************************************************************)
 359
 360 definition shift_i_L ≝ λsig,n,i.
 361    ncombf_r (multi_sig …) (shift_i sig n i) (all_blank sig n) ·
 362    mti sig n i ·
 363    extend ? (all_blank sig n).
 364
 365 definition R_shift_i_L ≝ λsig,n,i,t1,t2.
 366   (* ∀b:multi_sig sig n.∀ls.
 367     (t1 = midtape ? ls b [ ] →
 368      t2 = midtape (multi_sig sig n)
 369       ((shift_i sig n i b (all_blank sig n))::ls) (all_blank sig n) [ ]) ∧ *)
 370     (∀a,ls,rs.
 371       t1 = midtape ? ls a rs  →
 372       ((∃rs1,b,rs2,a1,rss.
 373         rs = rs1@b::rs2 ∧
 374         nth i ? (vec … b) (blank ?) = (blank ?) ∧
 375         (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 376         shift_l sig n i (a::rs1) (a1::rss) ∧
 377         t2 = midtape (multi_sig sig n) ((reverse ? (a1::rss))@ls) b rs2) ∨
 378       (∃b,rss.
 379         (∀x. mem ? x rs → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 380         shift_l sig n i (a::rs) (rss@[b]) ∧
 381         t2 = midtape (multi_sig sig n)
 382           ((reverse ? (rss@[b]))@ls) (all_blank sig n) [ ]))).
 383
 384 definition R_shift_i_L_new ≝ λsig,n,i,t1,t2.
 385   (∀a,ls,rs.
 386    t1 = midtape ? ls a rs  →
 387    ∃rs1,b,rs2,rss.
 388       b = hd ? rs2 (all_blank sig n) ∧
 389       nth i ? (vec … b) (blank ?) = (blank ?) ∧
 390       rs = rs1@rs2 ∧
 391       (∀x. mem ? x rs1 → nth i ? (vec … x) (blank ?) ≠ (blank ?)) ∧
 392       shift_l sig n i (a::rs1) rss ∧
 393       t2 = midtape (multi_sig sig n) ((reverse ? rss)@ls) b (tail ? rs2)).
 394
 395 theorem sem_shift_i_L: ∀sig,n,i. shift_i_L sig n i  ⊨ R_shift_i_L sig n i.
 396 #sig #n #i
 397 @(sem_seq_app ??????
 398   (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
 399    (sem_seq ????? (ssem_mti sig n i)
 400     (sem_extend ? (all_blank sig n))))
 401 #tin #tout * #t1 * * #Ht1a #Ht1b * #t2 * * #Ht2a #Ht2b * #Htout1 #Htout2
 402 (* #b #ls %
 403   [#Htin lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 404    lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 405    >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout // *)
 406 #a #ls #rs cases rs
 407   [#Htin %2 %{(shift_i sig n i a (all_blank sig n))} %{[ ]}
 408    %[%[#x @False_ind | @daemon]
 409     |lapply (Ht1a … Htin) -Ht1a -Ht1b #Ht1
 410      lapply (Ht2a … Ht1) -Ht2a -Ht2b #Ht2 >Ht2 in Htout1;
 411      >Ht1 whd in match (left ??); whd in match (right ??); #Htout @Htout //
 412     ]
 413   |#a1 #rs1 #Htin
 414    lapply (Ht1b … Htin) -Ht1a -Ht1b #Ht1
 415    lapply (Ht2b … Ht1) -Ht2a -Ht2b *
 416     [(* a1 is blank *) * #H1 #H2 %1
 417      %{[ ]} %{a1} %{rs1} %{(shift_i sig n i a a1)} %{[ ]}
 418      %[%[%[%[// |//] |#x @False_ind] | @daemon]
 419       |>Htout2 [>H2 >reverse_single @Ht1 |>H2 >Ht1 normalize % #H destruct (H)]
 420       ]
 421     |*
 422     [* #rs10 * #b * #rs2 * #rss * * * * #H1 #H2 #H3 #H4
 423      #Ht2 %1
 424      %{(a1::rs10)} %{b} %{rs2} %{(shift_i sig n i a a1)} %{rss}
 425      %[%[%[%[>H1 //|//] |@H3] |@daemon ]
 426       |>reverse_cons >associative_append
 427        >H2 in Htout2; #Htout >Htout [@Ht2| >Ht2 normalize % #H destruct (H)]
 428       ]
 429     |* #b * #rss * * #H1 #H2
 430      #Ht2 %2
 431      %{(shift_i sig n i b (all_blank sig n))} %{(shift_i sig n i a a1::rss)}
 432      %[%[@H1 |@daemon ]
 433       |>Ht2 in Htout1; #Htout >Htout //
 434        whd in match (left ??); whd in match (right ??);
 435        >reverse_append >reverse_single >associative_append  >reverse_cons
 436        >associative_append //
 437        ]
 438      ]
 439    ]
 440  ]
 441 qed.
 442
 443 theorem sem_shift_i_L_new: ∀sig,n,i.
 444   shift_i_L sig n i  ⊨ R_shift_i_L_new sig n i.
 445 #sig #n #i
 446 @(Realize_to_Realize … (sem_shift_i_L sig n i))
 447 #t1 #t2 #H #a #ls #rs #Ht1 lapply (H a ls rs Ht1) *
 448   [* #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
 449    %{rs1} %{b} %{(b::rs2)} %{(a1::rss)}
 450    %[%[%[%[%[//|@H2]|@H1]|@H3]|@H4] | whd in match (tail ??); @Ht2]
 451   |* #b * #rss * * #H1 #H2 #Ht2
 452    %{rs} %{(all_blank sig n)} %{[]} %{(rss@[b])}
 453    %[%[%[%[%[//|@blank_all_blank]|//]|@H1]|@H2] | whd in match (tail ??); @Ht2]
 454   ]
 455 qed.
 456
 457
 458 (******************************************************************************)
 459 definition no_head_in ≝ λsig,n,l.
 460   ∀x. mem ? x (trace sig n n l) → x ≠ head ?.
 461
 462 lemma no_head_true: ∀sig,n,a.
 463   nth n ? (vec … n a) (blank sig) ≠ head ? → no_head … a = true.
 464 #sig #n #a normalize cases (nth n ? (vec … n a) (blank sig))
 465 normalize // * normalize // * #H @False_ind @H //
 466 qed.
 467
 468 lemma no_head_false: ∀sig,n,a.
 469   nth n ? (vec … n a) (blank sig) = head ? → no_head … a = false.
 470 #sig #n #a #H normalize >H //
 471 qed.
 472
 473 definition mtiL ≝ λsig,n,i.
 474    move_to_blank_L sig n i ·
 475    shift_i_L sig n i ·
 476    move_until ? L (no_head sig n).
 477
 478 definition Rmtil ≝ λsig,n,i,t1,t2.
 479   ∀ls,a,rs.
 480    t1 = midtape (multi_sig sig n) ls a rs →
 481    nth n ? (vec … a) (blank ?) = head ? →
 482    no_head_in … ls →
 483    no_head_in … rs  →
 484    (∃ls1,a1,rs1.
 485      t2 = midtape (multi_sig …) ls1 a1 rs1 ∧
 486      (∀j. j ≤ n → j ≠ i → to_blank_i ? n j (a1::ls1) = to_blank_i ? n j (a::ls)) ∧
 487      (∀j. j ≤ n → j ≠ i → to_blank_i ? n j rs1 = to_blank_i ? n j rs) ∧
 488      (to_blank_i ? n i ls1 = to_blank_i ? n i (a::ls)) ∧
 489      (to_blank_i ? n i (a1::rs1)) = to_blank_i ? n i rs).
 490
 491 lemma reverse_map: ∀A,B,f,l.
 492   reverse B (map … f l) = map … f (reverse A l).
 493 #A #B #f #l elim l //
 494 #a #l #Hind >reverse_cons >reverse_cons <map_append >Hind //
 495 qed.
 496
 497 theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i  ⊨ Rmtil sig n i.
 498 #sig #n #i #lt_in
 499 @(sem_seq_app ??????
 500   (sem_move_to_blank_L_new … )
 501    (sem_seq ????? (sem_shift_i_L_new …)
 502     (ssem_move_until_L ? (no_head sig n))))
 503 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
 504 (* we start looking into Rmitl *)
 505 #ls #a #rs #Htin (* tin is a midtape *)
 506 #Hhead #Hnohead_ls #Hnohead_rs
 507 lapply (Ht1 … Htin) -Ht1 -Htin
 508 * #b * #ls1 * #ls2 * * * #Hno_blankb #Hhead #Hls1 #Ht1
 509 lapply (Ht2 … Ht1) -Ht2 -Ht1
 510 * #rs1 * #b0 * #rs2 * #rss * * * * * #Hb0 #Hb0blank #Hrs1 #Hrs1b #Hrss #Ht2
 511 (* we need to recover the position of the head of the emulated machine
 512    that is the head of ls1. This is somewhere inside rs1 *)
 513 cut (∃rs11. rs1 = (reverse ? ls1)@rs11)
 514      [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
 515        [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
 516        [#H1ls1 %{rs1} >H1ls1 //
 517        |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
 518         cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
 519         #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
 520          [* #H1 #H2 %{l} @H1
 521          |(* this is absurd : if l is empty, the case is as before.
 522            if l is not empty then it must start with a blank, since it is the
 523            frist character in rs2. But in this case we would have a blank
 524            inside ls1=attls1 that is absurd *)
 525           @daemon
 526          ]]]
 527    * #rs11 #H1
 528 lapply (Htout … Ht2) -Htout -Ht2 *
 529   [(* the current character on trace i hold the head-mark.
 530       The case is absurd, since b0 is the head of rs2, that is a sublist of rs,
 531       and the head-mark is not in rs *)
 532    @daemon
 533    (* something is missing
 534    * #H @False_ind @(absurd ? H) @eqnot_to_noteq whd in ⊢ (???%);
 535    cut (rs2 = [ ] ∨ ∃c,rs21. rs2 = c::rs21)
 536     [cases rs2 [ %1 // | #c #rs22 %2 %{c} %{rs22} //]]
 537    * (* by cases on rs2 *)
 538     [#Hrs2 >Hb0 >Hrs2 normalize >all_blank_n //
 539     |* #c * #rs22 #Hrs2 destruct (Hrs2) @no_head_true @Hnohead_rs
 540      > *)
 541   |*
 542   [(* we reach the head position *)
 543    (* cut (trace sig n j (a1::ls20)=trace sig n j (ls1@b::ls2)) *)
 544    * #ls10 * #a1 * #ls20 * * * #Hls20 #Ha1 #Hnh #Htout
 545    cut (∀j.j ≠ i →
 546       trace sig n j (reverse (multi_sig sig n) rs1@b::ls2) =
 547       trace sig n j (ls10@a1::ls20))
 548     [#j #ineqj >append_cons <reverse_cons >trace_def <map_append <reverse_map
 549      lapply (trace_shift_neq …lt_in ? (sym_not_eq … ineqj) … Hrss) [//] #Htr
 550      <(trace_def …  (b::rs1)) <Htr >reverse_map >map_append @eq_f @Hls20 ]
 551    #Htracej
 552    cut (trace sig n i (reverse (multi_sig sig n) (rs1@[b0])@ls2) =
 553         trace sig n i (ls10@a1::ls20))
 554     [>trace_def <map_append <reverse_map <map_append <(trace_def … [b0])
 555      cut (trace sig n i [b0] = [blank ?]) [@daemon] #Hcut >Hcut
 556      lapply (trace_shift … lt_in … Hrss) [//] whd in match (tail ??); #Htr <Htr
 557      >reverse_map >map_append <trace_def <Hls20 %
 558     ]
 559    #Htracei
 560    cut (∀j. j ≠ i →
 561       (trace sig n j (reverse (multi_sig sig n) rs11) = trace sig n j ls10) ∧
 562       (trace sig n j (ls1@b::ls2) = trace sig n j (a1::ls20)))
 563    [@daemon (* si fa
 564      #j #ineqj @(first_P_to_eq ? (λx. x ≠ head ?))
 565       [lapply (Htracej … ineqj) >trace_def in ⊢ (%→?); <map_append
 566        >trace_def in ⊢ (%→?); <map_append #H @H
 567       | *) ] #H2
 568   cut ((trace sig n i (b0::reverse ? rs11) = trace sig n i (ls10@[a1])) ∧
 569       (trace sig n i (ls1@ls2) = trace sig n i ls20))
 570     [>H1 in Htracei; >reverse_append >reverse_single >reverse_append
 571      >reverse_reverse >associative_append >associative_append
 572      @daemon
 573     ] #H3
 574    %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
 575    %[%[%[%[@Htout
 576     |#j #lejn #jneqi <(Hls1 … lejn)
 577      >to_blank_i_def >to_blank_i_def @eq_f @sym_eq @(proj2 … (H2 j jneqi))]
 578     |#j #lejn #jneqi >reverse_cons >associative_append >Hb0
 579      <to_blank_hd_cons >to_blank_i_def >to_blank_i_def @eq_f
 580      @(injective_append_l … (trace sig n j (reverse ? ls1))) (* >trace_def >trace_def *)
 581      >map_append >map_append >Hrs1 >H1 >associative_append
 582      <map_append <map_append in ⊢ (???%); @eq_f
 583      <map_append <map_append @eq_f2 // @sym_eq
 584      <(reverse_reverse … rs11) <reverse_map <reverse_map in ⊢ (???%);
 585      @eq_f @(proj1 … (H2 j jneqi))]
 586     |<(Hls1 i) [2:@lt_to_le //] (* manca un invariante: dopo un blank
 587      posso avere solo blank *) @daemon ]
 588     |>reverse_cons >associative_append
 589      cut (to_blank_i sig n i rs = to_blank_i sig n i (rs11@[b0])) [@daemon]
 590      #Hcut >Hcut >(to_blank_i_chop  … b0 (a1::reverse …ls10)) [2: @Hb0blank]
 591      >to_blank_i_def >to_blank_i_def @eq_f
 592      >trace_def >trace_def @injective_reverse >reverse_map >reverse_cons
 593      >reverse_reverse >reverse_map >reverse_append >reverse_single @sym_eq
 594      @(proj1 … H3)
 595     ]
 596   |(*we do not find the head: this is absurd *)
 597    * #b1 * #lss * * #H2 @False_ind
 598    cut (∀x0. mem ? x0 (trace sig n n (b0::reverse ? rss@ls2)) → x0 ≠ head ?)
 599      [@daemon] -H2 #H2
 600    lapply (trace_shift_neq sig n i n … lt_in … Hrss)
 601      [@lt_to_not_eq @lt_in | // ]
 602    #H3 @(absurd
 603         (nth n ? (vec … (hd ? (ls1@[b]) (all_blank sig n))) (blank ?) = head ?))
 604      [>Hhead //
 605      |@H2 >trace_def %2 <map_append @mem_append_l1 <reverse_map <trace_def
 606       >H3 >H1 >trace_def >reverse_map >reverse_cons >reverse_append
 607       >reverse_reverse >associative_append <map_append @mem_append_l2
 608       cases ls1 [%1 % |#x #ll %1 %]
 609      ]
 610
 611
 612
 613
 614 (*
 615
 616    cut (∀j.i ≠ j →
 617       trace sig n j (reverse (multi_sig sig n) rss@ls2) =
 618       trace sig n j (ls10@a1::ls20))
 619     [#j #ineqj >trace_def <map_append in ⊢ (??%?);
 620      <reverse_map lapply (trace_shift_neq …lt_in ? ineqj … Hrss) [//] #Htr
 621      <trace_def <trace_def >Htr >reverse_cons *)
 622
 623    %{ls20} %{a1} %{(reverse ? (b0::ls10)@tail (multi_sig sig n) rs2)}
 624    %[%[%[%[%[@Htout
 625     |#j #lejn #jneqi <(Hls1 … lejn) -Hls1
 626      >to_blank_i_def >to_blank_i_def @eq_f
 627      @(injective_append_l … (trace sig n j (reverse ? rs))) (* >trace_def >trace_def *)
 628      >map_append >map_append
 629
 630      ]
 631     |@daemon]
 632     |@daemon]
 633     |@daemon]
 634     |
 635
 636
 637   [(* the current character on trace i is blank *)
 638    * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2;
 639    #Ht2 lapply (Ht2 … (refl …)) *
 640     [(* we reach the margin of the i-th trace *)
 641      * #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
 642      lapply (Htout … Ht2) -Htout *
 643       [(* the head is on b: this is absurd *)
 644        * #Hhb @False_ind >Hnohead_rs in Hhb;
 645         [#H destruct (H) | >H1 @mem_append_l2 %1 //]
 646       |*
 647       [(* we reach the head position *)
 648        * #ls1 * #b0 * #ls2 * * * #H5 #H6 #H7 #Htout
 649        %{ls2} %{b0} %{(reverse ? (b::ls1)@rs2)}
 650        cut (ls2 = ls)
 651          [@daemon (* da finire
 652           lapply H5 lapply H4 -H5 -H4 cases rss
 653            [* normalize in ⊢ (%→?); #H destruct (H)
 654            |#rssa #rsstl #H >reverse_cons >associative_append
 655             normalize in ⊢ (??(???%)%→?); #H8 @sym_eq
 656             @(first_P_to_eq (multi_sig sig n)
 657               (λa.nth n (sig_ext sig) (vec … a) (blank ?) = head ?) ?????? H8)
 658           *)
 659          ] #Hls
 660        %[%[%[%[%[@Htout|>Hls //]
 661               | #j #lejn #neji >to_blank_i_def >to_blank_i_def
 662                @eq_f >H1 >trace_def >trace_def >reverse_cons
 663                >associative_append <map_append <map_append in ⊢ (???%); @eq_f2 //
 664                @daemon]
 665              |//]
 666            |* #H @False_ind @H @daemon
 667            ]
 668          |>H1 @daemon
 669          ]
 670      |(* we do not find the head: absurd *)
 671       cut (nth n (sig_ext sig) (vec … a1) (blank sig)=head sig)
 672         [lapply (trace_shift_neq ??? n … lt_in … H4)
 673           [@lt_to_not_eq // |//]
 674          whd in match (trace ????); whd in match (trace ???(a::rs1));
 675          #H <Hhead @(cons_injective_l … H)]
 676        #Hcut * #b0 * #lss * * #H @False_ind
 677        @(absurd (true=false)) [2://] <(H a1)
 678         [whd in match (no_head ???); >Hcut //
 679         |%2 @mem_append_l1 >reverse_cons @mem_append_l2 %1 //
 680         ]
 681      ]
 682
 683 theorem sem_Rmtil: ∀sig,n,i. i < n → mtiL sig n i  ⊨ Rmtil sig n i.
 684 #sig #n #i #lt_in
 685 @(sem_seq_app ??????
 686   (sem_move_to_blank_L … )
 687    (sem_seq ????? (sem_shift_i_L …)
 688     (ssem_move_until_L ? (no_head sig n))))
 689 #tin #tout * #t1 * * #_ #Ht1 * #t2 * #Ht2 * #_ #Htout
 690 (* we start looking into Rmitl *)
 691 #ls #a #rs #Htin (* tin is a midtape *)
 692 #Hhead #Hnohead_ls #Hnohead_rs
 693 cases (Ht1 … Htin) -Ht1
 694   [(* the current character on trace i is blank *)
 695    * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2;
 696    #Ht2 lapply (Ht2 … (refl …)) *
 697     [(* we reach the margin of the i-th trace *)
 698      * #rs1 * #b * #rs2 * #a1 * #rss * * * * #H1 #H2 #H3 #H4 #Ht2
 699      lapply (Htout … Ht2) -Htout *
 700       [(* the head is on b: this is absurd *)
 701        * #Hhb @False_ind >Hnohead_rs in Hhb;
 702         [#H destruct (H) | >H1 @mem_append_l2 %1 //]
 703       |*
 704       [(* we reach the head position *)
 705        * #ls1 * #b0 * #ls2 * * * #H5 #H6 #H7 #Htout
 706        %{ls2} %{b0} %{(reverse ? (b::ls1)@rs2)}
 707        cut (ls2 = ls)
 708          [@daemon (* da finire
 709           lapply H5 lapply H4 -H5 -H4 cases rss
 710            [* normalize in ⊢ (%→?); #H destruct (H)
 711            |#rssa #rsstl #H >reverse_cons >associative_append
 712             normalize in ⊢ (??(???%)%→?); #H8 @sym_eq
 713             @(first_P_to_eq (multi_sig sig n)
 714               (λa.nth n (sig_ext sig) (vec … a) (blank ?) = head ?) ?????? H8)
 715           *)
 716          ] #Hls
 717        %[%[%[%[%[@Htout|>Hls //]
 718               | #j #lejn #neji >to_blank_i_def >to_blank_i_def
 719                @eq_f >H1 >trace_def >trace_def >reverse_cons
 720                >associative_append <map_append <map_append in ⊢ (???%); @eq_f2 //
 721                @daemon]
 722              |//]
 723            |* #H @False_ind @H @daemon
 724            ]
 725          |>H1 @daemon
 726          ]
 727      |(* we do not find the head: absurd *)
 728       cut (nth n (sig_ext sig) (vec … a1) (blank sig)=head sig)
 729         [lapply (trace_shift_neq ??? n … lt_in … H4)
 730           [@lt_to_not_eq // |//]
 731          whd in match (trace ????); whd in match (trace ???(a::rs1));
 732          #H <Hhead @(cons_injective_l … H)]
 733        #Hcut * #b0 * #lss * * #H @False_ind
 734        @(absurd (true=false)) [2://] <(H a1)
 735         [whd in match (no_head ???); >Hcut //
 736         |%2 @mem_append_l1 >reverse_cons @mem_append_l2 %1 //
 737         ]
 738      ]
 739
 740
 741 theorem sem_Rmtil: ∀sig,n,i. mtiL sig n i  ⊨ Rmtil sig n i.
 742 #sig #n #i
 743 @(sem_seq_app ??????
 744   (ssem_move_until_L ? (no_blank sig n i))
 745    (sem_seq ????? (sem_extend ? (all_blank sig n))
 746     (sem_seq ????? (sem_ncombf_r (multi_sig sig n) (shift_i sig n i)(all_blank sig n))
 747      (sem_seq ????? (ssem_mti sig n i)
 748       (sem_seq ????? (sem_extend ? (all_blank sig n))
 749        (ssem_move_until_L ? (no_head sig n)))))))
 750 #tin #tout * #t1 * * #_ #Ht1 * #t2 * * #Ht2a #Ht2b * #t3 * * #Ht3a #Ht3b
 751 * #t4 * * #Ht4a #Ht4b * #t5 * * #Ht5a #Ht5b * #t6 #Htout
 752 (* we start looking into Rmitl *)
 753 #ls #a #rs #Htin (* tin is a midtape *)
 754 #Hhead #Hnohead_ls #Hnohead_rs
 755 cases (Ht1 … Htin) -Ht1
 756   [(* the current character on trace i is blank *)
 757    -Ht2a * #Hblank #Ht1 <Ht1 in Htin; #Ht1a >Ht1a in Ht2b;
 758    #Ht2b lapply (Ht2b ?) [% normalize #H destruct] -Ht2b -Ht1 -Ht1a
 759    lapply Hnohead_rs -Hnohead_rs
 760    (* by cases on rs *) cases rs
 761     [#_ (* rs is empty *) #Ht2 -Ht3b lapply (Ht3a … Ht2)
 762      #Ht3 -Ht4b lapply (Ht4a … Ht3) -Ht4a #Ht4 -Ht5b
 763      >Ht4 in Ht5a; >Ht3 #Ht5a lapply (Ht5a (refl … )) -Ht5a #Ht5
 764      cases (Htout … Ht5) -Htout
 765       [(* the current symbol on trace n is the head: this is absurd *)
 766        * whd in ⊢ (??%?→?); >all_blank_n whd in ⊢ (??%?→?); #H destruct (H)
 767       |*
 768       [(* we return to the head *)
 769        * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
 770        #H1 #H2 #H3
 771        (* ls1 must be empty *)
 772        cut (ls1=[])
 773         [lapply H3 lapply H1 -H3 -H1 cases ls1 // #c #ls3
 774          whd in ⊢ (???%→?); #H1 destruct (H1)
 775          >blank_all_blank [|@daemon] #H @False_ind
 776          lapply (H … (change_vec (sig_ext sig) n a (blank sig) i) ?)
 777           [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 778            >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
 779        #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
 780        >reverse_single >blank_all_blank [|@daemon]
 781        whd in match (right ??) ; >append_nil #Htout
 782        %{ls2} %{(change_vec (sig_ext sig) n a (blank sig) i)} %{[all_blank sig n]}
 783        %[%[%[%[%[//|//]|@daemon]|//] |(*absurd*)@daemon]
 784         |normalize >nth_change_vec // @daemon]
 785       |(* we do not find the head: this is absurd *)
 786        * #b * #lss * * whd in match (left ??); #HF @False_ind
 787        lapply (HF … (shift_i sig n i a (all_blank sig n)) ?) [%2 %1 //]
 788        whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 789        >Hhead whd in ⊢ (??%?→?); #H destruct (H)
 790       ]
 791       ]
 792     |(* rs = c::rs1 *)
 793      #c #rs1 #Hnohead_rs #Ht2 -Ht3a lapply (Ht3b … Ht2) -Ht3b
 794      #Ht3 -Ht4a lapply (Ht4b … Ht3) -Ht4b *
 795       [(* the first character is blank *) *
 796        #Hblank #Ht4 -Ht5a >Ht4 in Ht5b; >Ht3
 797        normalize in ⊢ ((%→?)→?); #Ht5 lapply (Ht5 ?) [% #H destruct (H)]
 798        -Ht2 -Ht3 -Ht4 -Ht5 #Ht5 cases (Htout … Ht5) -Htout
 799         [(* the current symbol on trace n is the head: this is absurd *)
 800          * >Hnohead_rs [#H destruct (H) |%1 //]
 801         |*
 802         [(* we return to the head *)
 803          * #ls1 * #b * #ls2 * * * whd in ⊢ (??%?→?);
 804          #H1 #H2 #H3
 805          (* ls1 must be empty *)
 806          cut (ls1=[])
 807           [lapply H3 lapply H1 -H3 -H1 cases ls1 // #x #ls3
 808            whd in ⊢ (???%→?); #H1 destruct (H1) #H @False_ind
 809            lapply (H (change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i) ?)
 810             [%2 %1 // | whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 811              >Hhead whd in ⊢ (??%?→?); #H1 destruct (H1)]]
 812          #Hls1_nil >Hls1_nil in H1; whd in ⊢ (???%→?); #H destruct (H)
 813          >reverse_single #Htout
 814          %{ls2} %{(change_vec (sig_ext sig) n a (nth i (sig_ext sig) (vec … c) (blank sig)) i)}
 815          %{(c::rs1)}
 816          %[%[%[%[%[@Htout|//]|//]|//] |(*absurd*)@daemon]
 817           |>to_blank_cons_b
 818              [>(to_blank_cons_b … Hblank) //| >nth_change_vec [@Hblank |@daemon]]
 819           ]
 820         |(* we do not find the head: this is absurd *)
 821          * #b * #lss * * #HF @False_ind
 822          lapply (HF … (shift_i sig n i a c) ?) [%2 %1 //]
 823          whd in match (no_head ???); >nth_change_vec_neq [|@daemon]
 824          >Hhead whd in ⊢ (??%?→?); #H destruct (H)
 825         ]
 826       ]
 827     |
 828
 829   (* end of the first case !! *)
 830
 831
 832
 833    #Ht2
 834
 835 cut (∃rs11,rs12. b::rs1 = rs11@a::rs12 ∧ no_head_in ?? rs11)
 836      [cut (ls1 = [ ] ∨ ∃aa,tlls1. ls1 = aa::tlls1)
 837        [cases ls1 [%1 // | #aa #tlls1 %2 %{aa} %{tlls1} //]] *
 838        [#H1ls1 %{[ ]} %{rs1} %
 839          [ @eq_f2 // >H1ls1 in Hls1; whd in match ([]@b::ls2);
 840            #Hls1 @(to_blank_hd … Hls1)
 841          |normalize #x @False_ind
 842          ]
 843        |* #aa * #tlls1 #H1ls1 >H1ls1 in Hrs1;
 844         cut (aa = a) [>H1ls1 in Hls1; #H @(to_blank_hd … H)] #eqaa >eqaa
 845         #Hrs1_aux cases (compare_append … (sym_eq … Hrs1_aux)) #l *
 846          [* #H1 #H2 %{(b::(reverse ? tlls1))} %{l} %
 847            [@eq_f >H1 >reverse_cons >associative_append //
 848            |@daemon (* is a sublit of the tail of ls1, and hence of ls *)
 849            ]
 850          |(* this is absurd : if l is empty, the case is as before.
 851            if l is not empty then it must start with a blank, since it is the
 852            frist character in rs2. But in this case we would have a blank
 853            inside ls1=attls1 that is absurd *)
 854           @daemon
 855          ]]]
 856
 857