-definition tape_move_left ≝ λsig:FinSet.λlt:list sig.λc:sig.λrt:list sig.
- match lt with
- [ nil ⇒ leftof sig c rt
- | cons c0 lt0 ⇒ midtape sig lt0 c0 (c::rt) ].
+definition tape_move_left ≝ λsig:FinSet.λt:tape sig.
+ match t with
+ [ niltape ⇒ niltape sig
+ | leftof _ _ ⇒ t
+ | rightof a ls ⇒ midtape sig ls a [ ]
+ | midtape ls a rs ⇒
+ match ls with
+ [ nil ⇒ leftof sig a rs
+ | cons a0 ls0 ⇒ midtape sig ls0 a0 (a::rs)
+ ]
+ ].
+
+definition tape_move_right ≝ λsig:FinSet.λt:tape sig.
+ match t with
+ [ niltape ⇒ niltape sig
+ | rightof _ _ ⇒ t
+ | leftof a rs ⇒ midtape sig [ ] a rs
+ | midtape ls a rs ⇒
+ match rs with
+ [ nil ⇒ rightof sig a ls
+ | cons a0 rs0 ⇒ midtape sig (a::ls) a0 rs0
+ ]
+ ].