+definition tape_move ≝ λsig.λt: tape sig.λm:option (sig × move).
+ match m with
+ [ None ⇒ t
+ | Some m' ⇒
+ let 〈s,m1〉 ≝ m' in
+ match m1 with
+ [ R ⇒ tape_move_right ? (left ? t) s (right ? t)
+ | L ⇒ tape_move_left ? (left ? t) s (right ? t)
+ | N ⇒ midtape ? (left ? t) s (right ? t)
+ ] ].
+(*
+ (None,[]) → □
+ (None,a::[]) → □
+ (None,a::b::rs) → None::b::rs
+ (Some a,[]) → [Some a]
+ (Some a,b::rs) → Some a::rs
+ *)
+(*
+definition option_cons ≝ λA.λa:option A.λl.
+ match a with
+ [ None ⇒ match l with
+ [ nil ⇒ []
+ | cons _ _ ⇒ a::l ]
+ | Some _ ⇒ a::l ].
+
+(* definition tape_update := λsig.λt: tape sig.λs:option sig.
+ let newright ≝
+ match right ? t with
+ [ nil ⇒ match s with
+ [ None ⇒ []
+ | Some a ⇒ [Some ? a] ]
+ | cons b rs ⇒ match s with
+ [ None ⇒ match rs with
+ [ nil ⇒ []
+ | cons _ _ ⇒ None ?::rs ]
+ | Some a ⇒ Some ? a::rs ] ]
+ in mk_tape ? (left ? t) newright. *)
+
+definition tape_move ≝ λsig.λt:tape sig.λm:option sig × move.
+ let 〈s,m1〉 ≝ m in match m1 with
+ [ R ⇒ mk_tape sig (option_cons ? s (left ? t)) (tail ? (right ? t))
+ | L ⇒ mk_tape sig (tail ? (left ? t))
+ (option_cons ? (option_hd ? (left ? t))
+ (option_cons ? s (tail ? (right ? t))))
+ | N ⇒ mk_tape sig (left ? t) (option_cons ? s (tail ? (right ? t)))
+ ].
+*)
+