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