- [ O ⇒ 〈mmove1,change_vec ? (S n) (null_action ? n) (〈None ?,D〉) i〉
- | S _ ⇒ 〈mmove1,null_action sig n〉 ].
+ [ O ⇒ 〈smove1,None sig, D〉
+ | S _ ⇒ 〈smove1,None sig, N〉 ].
+
+definition move ≝
+ λsig,D.mk_TM sig smove_states (trans_smove sig D) smove0 (λq.q == smove1).
+
+definition mmove ≝ λi,sig,n,D.inject_TM sig (move sig D) n i.
+
+definition Rmove ≝
+ λalpha,D,t1,t2. t2 = tape_move alpha t1 D.
+
+lemma sem_move_single :
+ ∀alpha,D.move alpha D ⊨ Rmove alpha D.
+#alpha #D #int %{2} %{(mk_config ? smove_states smove1 ?)} [| % % ]
+qed.