-(* MOVE RIGHT
-
- moves the head one step to the right
-
-*)
-
-definition move_states ≝ initN 2.
-
-definition move_r ≝
- λalpha:FinSet.mk_TM alpha move_states
- (λp.let 〈q,a〉 ≝ p in
- match a with
- [ None ⇒ 〈1,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ 〈1,Some ? 〈a',R〉〉
- | S q ⇒ 〈1,None ?〉 ] ])
- O (λq.q == 1).
-
-definition R_move_r ≝ λalpha,t1,t2.
- ∀ls,c,rs.
- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (c::ls) (option_hd ? rs) (tail ? rs).
-
-lemma sem_move_r :
- ∀alpha.Realize ? (move_r alpha) (R_move_r alpha).
-#alpha #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-| #ls #c #rs
- @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
- cases rs0 // ] ] ]
-qed.
-
-(* MOVE LEFT
-
- moves the head one step to the right
-
-*)
-
-definition move_l ≝
- λalpha:FinSet.mk_TM alpha move_states
- (λp.let 〈q,a〉 ≝ p in
- match a with
- [ None ⇒ 〈1,None ?〉
- | Some a' ⇒ match q with
- [ O ⇒ 〈1,Some ? 〈a',L〉〉
- | S q ⇒ 〈1,None ?〉 ] ])
- O (λq.q == 1).
-
-definition R_move_l ≝ λalpha,t1,t2.
- ∀ls,c,rs.
- t1 = midtape alpha ls c rs →
- t2 = mk_tape ? (tail ? ls) (option_hd ? ls) (c::rs).
-
-lemma sem_move_l :
- ∀alpha.Realize ? (move_l alpha) (R_move_l alpha).
-#alpha #intape @(ex_intro ?? 2) cases intape
-[ @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-|#a #al @ex_intro
- [| % [ % | #ls #c #rs #Hfalse destruct ] ]
-| #ls #c #rs
- @ex_intro [| % [ % | #ls0 #c0 #rs0 #H1 destruct (H1)
- cases ls0 // ] ] ]
-qed.