+ | Some x ⇒ notb (nth dst (DeqOption sig) v (None ?) == None ?) ].
+
+definition rewind ≝ λsrc,dst,sig,n.parmove src dst sig n L · parmove_step src 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).
+
+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
+check acc_sem_seq_app
+@(sem_seq_app sig n ????? (sem_parmoveL src dst sig n Hneq Hsrc Hdst)
+ (accRealize_to_Realize … (sem_parmove_step src dst sig n R Hneq Hsrc Hdst)))
+#ta #tb * #tc * * #HR1 #_ #HR2
+#x #x0 #xs #rs #Hmidta_src #ls0 #y #y0 #target #rs0 #Hlen #Hmidta_dst
+>(HR1 ??? Hmidta_src ls0 y (target@[y0]) rs0 ??) in HR2;
+[|>Hmidta_dst //
+|>length_append >length_append >Hlen % ] *
+[ whd in ⊢ (%→?); * #x1 * #x2 * *
+ >change_vec_commute in ⊢ (%→?); // >nth_change_vec //
+ cases (reverse sig (xs@[x0])@x::rs)
+ [|#z #zs] normalize in ⊢ (%→?); #H destruct (H)
+| whd in ⊢ (%→?); * #_ #Htb >Htb -Htb FAIL
+
+ normalize in ⊢ (%→?);
+ (sem_parmove_step src dst sig n R Hneq Hsrc Hdst))
+ (acc_sem_if ? n … (sem_partest sig n (match_test src dst sig ?))
+ (sem_seq …
+ (sem_parmoveL ???? Hneq Hsrc Hdst)
+ (sem_inject … dst (le_S_S_to_le … Hdst) (sem_move_r ? )))
+ (sem_nop …)))
+