Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
fixed counterexample according to def in Chap 8
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Mon, 01 Apr 2013 18:15:00 +0100
changeset 234 ca2ea835c363
parent 233 e0a7ee9842d6
child 235 0b9c893cfd1b
fixed counterexample according to def in Chap 8
Paper/Paper.thy file | annotate | diff | comparison | revisions
paper.pdf file | annotate | diff | comparison | revisions 
--- a/Paper/Paper.thy	Fri Mar 29 02:40:38 2013 +0000
+++ b/Paper/Paper.thy	Mon Apr 01 18:15:00 2013 +0100
@@ -1577,8 +1577,8 @@
   \noindent
   If started with standard tape @{term "([], [Oc])"}, it halts with the
   non-standard tape @{term "([Oc, Bk], [])"} according to the definition in Chapter 3---so no
-  result is calculated; but with the standard tape @{term "([], [Oc])"} according to the 
-  definition in Chapter 8. ???? 
+  result is calculated; but with the standard tape @{term "([Bk], [Oc])"} according to the 
+  definition in Chapter 8. 
   We solve this inconsistency in our formalisation by
   setting up our definitions so that the @{text counter_example} Turing machine does not 
   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 
Binary file paper.pdf has changed
tm