| 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