+
+definition mmove_states ≝ initN 2.
+
+definition mmove0 : mmove_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 2 (refl …)).
+definition mmove1 : mmove_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 2 (refl …)).
+
+definition trans_mmove ≝
+ λi,sig,n,D.
+ λp:mmove_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in match (pi1 … q) with
+ [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
+ | S _ ⇒ 〈mmove1,null_action sig n〉 ].
+
+definition mmove ≝
+ λi,sig,n,D.
+ mk_mTM sig n mmove_states (trans_mmove i sig n D)
+ mmove0 (λq.q == mmove1).
+
+definition Rm_multi ≝
+ λalpha,n,i,D.λt1,t2:Vector ? (S n).
+ t2 = change_vec ? (S n) t1 (tape_move alpha (nth i ? t1 (niltape ?)) D) i.
+
+lemma sem_move_multi :
+ ∀alpha,n,i,D.i ≤ n →
+ mmove i alpha n D ⊨ Rm_multi alpha n i D.
+#alpha #n #i #D #Hin #int %{2}
+%{(mk_mconfig ? mmove_states n mmove1 ?)}
+[| %
+ [ whd in ⊢ (??%?); @eq_f whd in ⊢ (??%?); @eq_f %
+ | whd >tape_move_multi_def
+ <(change_vec_same … (ctapes …) i (niltape ?))
+ >pmap_change <tape_move_multi_def >tape_move_null_action % ] ]
+ qed.