equal
deleted
inserted
replaced
61 - position of head (int) |
61 - position of head (int) |
62 - tape (int \<rightharpoonup> Block) |
62 - tape (int \<rightharpoonup> Block) |
63 *) |
63 *) |
64 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
64 type_synonym tconf = "nat \<times> (nat \<rightharpoonup> tm_inst) \<times> nat \<times> int \<times> (int \<rightharpoonup> Block)" |
65 |
65 |
|
66 (* updates the position/tape according to an action *) |
66 fun |
67 fun |
67 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
68 next_tape :: "taction \<Rightarrow> (int \<times> (int \<rightharpoonup> Block)) \<Rightarrow> (int \<times> (int \<rightharpoonup> Block))" |
68 where |
69 where |
69 "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" | |
70 "next_tape W0 (pos, m) = (pos, m(pos \<mapsto> Bk))" | |
70 "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" | |
71 "next_tape W1 (pos, m) = (pos, m(pos \<mapsto> Oc))" | |