+lemma sem_move_tape_l : Realize ? move_tape_l R_move_tape_l.
+#tapein
+cases (sem_seq … sem_ml_atml
+ (sem_seq … sem_ml_atml
+ (sem_seq … (sem_move_l …)
+ (sem_seq … sem_init_cell
+ (sem_seq … sem_mtl_aux
+ (sem_seq … (sem_swap_r STape 〈grid,false〉)
+ (sem_seq … sem_mtl_aux
+ (sem_seq … (sem_swap STape 〈grid,false〉)
+ (sem_seq … sem_ml_atml sem_ml_atml)))))))) tapein)
+#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#rs #n #table #c0 #bc0 #curconfig #ls0 #Hbitnullc0 #Hbitnullcc #Htable #Hls0 #Htapein
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Htapein)
+[ @daemon (* by no_grids_in_table, manca un lemma sulla reverse *) ]
+-Hta #Hta * #tb * whd in ⊢ (%→?); #Htb lapply (Htb (〈c0,bc0〉::curconfig) … Hta)
+[ @daemon ] -Hta -Htb #Htb
+* #tc * whd in ⊢ (%→?); #Htc lapply (Htc … Htb) -Htb -Htc #Htc
+* #td * whd in ⊢ (%→?); *
+[ * #c1 * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
+ cases ls0 in Hls0;
+ [ #_ #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ #l1 #ls1 #Hls0 #Htapein #Htc change with (midtape ? ls1 l1 ?) in Htc:(???%); >Htc
+ #Hl1 whd in Hl1:(??%?); #Htd
+ * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
+ [ (* memb_reverse *) @daemon ] -Hte -Htd >reverse_reverse #Hte
+ * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+ * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
+ [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
+ * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
+ * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
+ [ (* memb_reverse *) @daemon ] -Hti -Hth #Hti
+ whd in ⊢ (%→?); #Houtc lapply (Houtc (l1::curconfig) … Hti)
+ [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) lapply (Hls0 l1 (memb_hd …)) @bit_not_grid
+ | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ]
+ -Houtc >reverse_cons >associative_append #Houtc %2 %{l1} %{ls1} % [%] @Houtc
+| * generalize in match Htc; generalize in match Htapein; -Htapein -Htc
+ cases ls0
+ [| #l1 #ls1 #_ #Htc >Htc normalize in ⊢ (%→?); #Hfalse destruct (Hfalse) ]
+ #Htapein #Htc change with (leftof ???) in Htc:(???%); >Htc #_ #Htd
+ * #te * whd in ⊢ (%→?); #Hte lapply (Hte … Htd ?)
+ [ (*memb_reverse*) @daemon ] -Hte -Htd >reverse_reverse #Hte
+ * #tf * whd in ⊢ (%→?); #Htf lapply (Htf … Hte) -Htf -Hte #Htf
+ * #tg * whd in ⊢ (%→?); #Htg lapply (Htg … Htf ?)
+ [ @(no_grids_in_table … Htable) ] -Htg -Htf >reverse_reverse #Htg
+ * #th * whd in ⊢ (%→?); #Hth lapply (Hth … Htg) -Hth -Htg #Hth
+ * #ti * whd in ⊢ (%→?); #Hti lapply (Hti … Hth)
+ [ (*memb_reverse*) @daemon ] -Hti -Hth #Hti
+ whd in ⊢ (%→?); #Houtc lapply (Houtc (〈null,false〉::curconfig) … Hti)
+ [ #x #Hx cases (orb_true_l … Hx) -Hx #Hx
+ [ >(\P Hx) %
+ | lapply (Hbitnullcc ? Hx) @bit_or_null_not_grid ] ]
+ -Houtc >reverse_cons >associative_append
+ >reverse_cons >associative_append #Houtc % % [%] @Houtc
+]
+qed.
+
+(*definition mtl_aux ≝
+ seq ? (move_r …) (seq ? (move_char_c STape 〈grid,false〉) (move_l …)).
+definition R_mtl_aux ≝ λt1,t2.
+ ∀l1,l2,l3,r. t1 = midtape STape l1 r (l2@〈grid,false〉::l3) → no_grids l2 →
+ t2 = midtape STape (reverse ? l2@l1) r (〈grid,false〉::l3).
+
+lemma sem_mtl_aux : Realize ? mtl_aux R_mtl_aux.
+#intape
+cases (sem_seq … (sem_move_r …) (sem_seq … (ssem_move_char_c STape 〈grid,false〉) (sem_move_l …)) intape)
+#k * #outc * #Hloop #HR @(ex_intro ?? k) @(ex_intro ?? outc) % [@Hloop] -Hloop
+#l1 #l2 #l3 #r #Hintape #Hl2
+cases HR -HR #ta * whd in ⊢ (%→?); #Hta lapply (Hta … Hintape) -Hta #Hta
+* #tb * whd in ⊢(%→?); generalize in match Hta; -Hta cases l2 in Hl2;
+[ #_ #Hta #Htb lapply (Htb … Hta) -Htb * #Htb #_ whd in ⊢ (%→?); #Houtc
+ lapply (Htb (refl ??)) -Htb >Hta @Houtc
+| #c0 #l0 #Hnogrids #Hta #Htb lapply (Htb … Hta) -Htb * #_ #Htb
+ lapply (Htb … (refl ??) ??)
+ [ cases (true_or_false (memb STape 〈grid,false〉 l0)) #Hmemb
+ [ @False_ind lapply (Hnogrids 〈grid,false〉 ?)
+ [ @memb_cons // | normalize #Hfalse destruct (Hfalse) ]
+ | @Hmemb ]
+ | % #Hc0 lapply (Hnogrids c0 ?)
+ [ @memb_hd | >Hc0 normalize #Hfalse destruct (Hfalse) ]
+ | #Htb whd in ⊢(%→?); >Htb #Houtc lapply (Houtc … (refl ??)) -Houtc #Houtc
+ >reverse_cons >associative_append @Houtc
+]]
+qed.
+
+check swap*)
+