+definition copy_char_states ≝ initN 3.
+
+definition cc0 : copy_states ≝ mk_Sig ?? 0 (leb_true_to_le 1 3 (refl …)).
+definition cc1 : copy_states ≝ mk_Sig ?? 1 (leb_true_to_le 2 3 (refl …)).
+
+definition trans_copy_char ≝
+ λsrc,dst.λsig:FinSet.λn.
+ λp:copy_char_states × (Vector (option sig) (S n)).
+ let 〈q,a〉 ≝ p in
+ match pi1 … q with
+ [ O ⇒ 〈cc1,change_vec ? (S n)
+ (change_vec ? (S n) (null_action ? n) (〈None ?,R〉) src)
+ (〈nth src ? a (None ?),R〉) dst〉
+ | S _ ⇒ 〈cc1,null_action ? n〉 ].
+
+definition copy_char ≝
+ λsrc,dst,sig,n.
+ mk_mTM sig n copy_char_states (trans_copy_char src dst sig n)
+ cc0 (λq.q == cc1).
+
+definition R_copy_char ≝
+ λsrc,dst,sig,n.λint,outt: Vector (tape sig) (S n).
+ outt = change_vec ??
+ (change_vec ?? int
+ (tape_move_mono ? (nth src ? int (niltape ?)) 〈None ?, R〉) src)
+ (tape_move_mono ? (nth dst ? int (niltape ?))
+ 〈current ? (nth src ? int (niltape ?)), R〉) dst.
+
+lemma copy_char_q0_q1 :
+ ∀src,dst,sig,n,v.src ≠ dst → src < S n → dst < S n →
+ step sig n (copy_char src dst sig n) (mk_mconfig ??? cc0 v) =
+ mk_mconfig ??? cc1
+ (change_vec ? (S n)
+ (change_vec ?? v
+ (tape_move_mono ? (nth src ? v (niltape ?)) 〈None ?, R〉) src)
+ (tape_move_mono ? (nth dst ? v (niltape ?)) 〈current ? (nth src ? v (niltape ?)), R〉) dst).
+#src #dst #sig #n #v #Heq #Hsrc #Hdst
+whd in ⊢ (??%?);
+<(change_vec_same … v dst (niltape ?)) in ⊢ (??%?);
+<(change_vec_same … v src (niltape ?)) in ⊢ (??%?);
+>tape_move_multi_def @eq_f2 //
+>pmap_change >pmap_change <tape_move_multi_def
+>tape_move_null_action @eq_f2 // @eq_f2
+[ >change_vec_same %
+| >change_vec_same >change_vec_same // ]
+qed.
+
+lemma sem_copy_char:
+ ∀src,dst,sig,n.src ≠ dst → src < S n → dst < S n →
+ copy_char src dst sig n ⊨ R_copy_char src dst sig n.
+#src #dst #sig #n #Hneq #Hsrc #Hdst #int
+%{2} % [| % [ % | whd >copy_char_q0_q1 // ]]
+qed.
+