+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.
+
+definition rewind ≝ λsrc,dst,sig,n.
+ parmove src dst sig n L · mmove src sig n R · mmove dst sig n R.
+
+definition R_rewind ≝ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ (∀x,x0,xs,rs.
+ nth src ? int (niltape ?) = midtape sig (xs@[x0]) x rs →
+ ∀ls0,y,y0,target,rs0.|xs| = |target| →
+ nth dst ? int (niltape ?) = midtape sig (target@y0::ls0) y rs0 →
+ outt = change_vec ??
+ (change_vec ?? int (midtape sig [] x0 (reverse ? xs@x::rs)) src)
+ (midtape sig ls0 y0 (reverse ? target@y::rs0)) dst) ∧
+ (∀x,rs.nth src ? int (niltape ?) = midtape sig [] x rs →
+ ∀ls0,y,rs0.nth dst ? int (niltape ?) = midtape sig ls0 y rs0 →
+ outt = int).
+
+(*
+theorem accRealize_to_Realize :
+ ∀sig,n.∀M:mTM sig n.∀Rtrue,Rfalse,acc.
+ M ⊨ [ acc: Rtrue, Rfalse ] → M ⊨ Rtrue ∪ Rfalse.
+#sig #n #M #Rtrue #Rfalse #acc #HR #t
+cases (HR t) #k * #outc * * #Hloop
+#Htrue #Hfalse %{k} %{outc} % //
+cases (true_or_false (cstate sig (states sig n M) n outc == acc)) #Hcase
+[ % @Htrue @(\P Hcase) | %2 @Hfalse @(\Pf Hcase) ]
+qed.
+*)
+
+lemma sem_rewind : ∀src,dst,sig,n.
+ src ≠ dst → src < S n → dst < S n →
+ rewind src dst sig n ⊨ R_rewind src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst
+@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst) ?)
+[| @(sem_seq_app sig n ????? (sem_move_multi … R ?) (sem_move_multi … R ?)) //
+ @le_S_S_to_le // ]
+#ta #tb * #tc * * #Htc #_ * #td * whd in ⊢ (%→%→?); #Htd #Htb %
+[ #x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst
+ >(Htc ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in Htd;
+ [|>Hmidta_dst //
+ |>length_append >length_append >Hlen % ]
+ >change_vec_commute [|@sym_not_eq //]
+ >change_vec_change_vec
+ >nth_change_vec_neq [|@sym_not_eq //]
+ >nth_change_vec // >reverse_append >reverse_single
+ >reverse_append >reverse_single normalize in match (tape_move ???);
+ >rev_append_def >append_nil #Htd >Htd in Htb;
+ >change_vec_change_vec >nth_change_vec //
+ cases ls0 [|#l1 #ls1] normalize in match (tape_move ???); //
+| #x #rs #Hmidta_src #ls0 #y #rs0 #Hmidta_dst
+ lapply (Htc … Hmidta_src … (refl ??) Hmidta_dst) -Htc #Htc >Htc in Htd;
+ >change_vec_commute [|@sym_not_eq //] >change_vec_change_vec
+ >nth_change_vec_neq [|@sym_not_eq //]
+ >nth_change_vec // lapply (refl ? ls0) cases ls0 in ⊢ (???%→%);
+ [ #Hls0 #Htd >Htd in Htb;
+ >nth_change_vec // >change_vec_change_vec
+ whd in match (tape_move ???);whd in match (tape_move ???); <Hmidta_src
+ <Hls0 <Hmidta_dst >change_vec_same >change_vec_same //
+ | #l1 #ls1 #Hls0 #Htd >Htd in Htb;
+ >nth_change_vec // >change_vec_change_vec
+ whd in match (tape_move ???);whd in match (tape_move ???); <Hmidta_src
+ <Hls0 <Hmidta_dst >change_vec_same >change_vec_same //
+]]
+qed.
+
+definition match_step ≝ λsrc,dst,sig,n.
+ compare src dst sig n ·
+ (ifTM ?? (partest sig n (match_test src dst sig ?))