equal
deleted
inserted
replaced
35 apply(rule_tac [!] eq_reflection) |
35 apply(rule_tac [!] eq_reflection) |
36 apply(auto split: taction.splits simp add: new_tape.simps) |
36 apply(auto split: taction.splits simp add: new_tape.simps) |
37 done |
37 done |
38 |
38 |
39 lemma tstep_def2: |
39 lemma tstep_def2: |
40 shows "tstep (s, l, []) p = (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))" |
40 shows "tstep (s, l, []) p == (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))" |
41 and "tstep (s, l, x#xs) p = (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))" |
41 and "tstep (s, l, x#xs) p == (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))" |
|
42 apply - |
|
43 apply(rule_tac [!] eq_reflection) |
42 by (auto split: prod.split list.split simp add: tstep.simps) |
44 by (auto split: prod.split list.split simp add: tstep.simps) |
43 |
45 |
44 consts DUMMY::'a |
46 consts DUMMY::'a |
45 |
47 |
46 notation (latex output) |
48 notation (latex output) |