V_____________________________________________________________*)
include "basics/vectors.ma".
+include "basics/finset.ma".
(* include "basics/relations.ma". *)
(******************************** tape ****************************************)
| cons r0 rs0 ⇒ leftof ? r0 rs0 ]
| cons l0 ls0 ⇒ rightof ? l0 ls0 ] ].
+lemma right_mk_tape :
+ ∀sig,ls,c,rs.(c = None ? → ls = [ ] ∨ rs = [ ]) → right ? (mk_tape sig ls c rs) = rs.
+#sig #ls #c #rs cases c // cases ls
+[ cases rs //
+| #l0 #ls0 #H normalize cases (H (refl ??)) #H1 [ destruct (H1) | >H1 % ] ]
+qed-.
+
+lemma left_mk_tape : ∀sig,ls,c,rs.left ? (mk_tape sig ls c rs) = ls.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
+lemma current_mk_tape : ∀sig,ls,c,rs.current ? (mk_tape sig ls c rs) = c.
+#sig #ls #c #rs cases c // cases ls // cases rs //
+qed.
+
lemma current_to_midtape: ∀sig,t,c. current sig t = Some ? c →
∃ls,rs. t = midtape ? ls c rs.
#sig *
| N ⇒ t
].
+definition tape_move_mono ≝
+ λsig,t,mv.
+ tape_move sig (tape_write sig t (\fst mv)) (\snd mv).
+
record config (sig,states:FinSet): Type[0] ≝
{ cstate : states;
ctape: tape sig
let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
+(*
+lemma step_eq : ∀sig,M,c.
+ let current_char ≝ current ? (ctape ?? c) in
+ let 〈news,a,mv〉 ≝ trans sig M 〈cstate ?? c,current_char〉 in
+ step sig M c =
+ mk_config ?? news (tape_move sig (tape_write ? (ctape ?? c) a) mv).
+#sig #M #c
+ whd in match (tape_move_mono sig ??);
+*)
+
(******************************** loop ****************************************)
let rec loop (A:Type[0]) n (f:A→A) p a on n ≝
match n with