1575   \end{center}

  1575   \end{center}

  1576 

  1576 

  1577   \noindent

  1577   \noindent

  1578   If started with standard tape @{term "([], [Oc])"}, it halts with the

  1578   If started with standard tape @{term "([], [Oc])"}, it halts with the

  1579   non-standard tape @{term "([Oc, Bk], [])"} according to the definition in Chapter 3---so no

  1579   non-standard tape @{term "([Oc, Bk], [])"} according to the definition in Chapter 3---so no

  1582   We solve this inconsistency in our formalisation by

  1582   We solve this inconsistency in our formalisation by

  1583   setting up our definitions so that the @{text counter_example} Turing machine does not 

  1583   setting up our definitions so that the @{text counter_example} Turing machine does not 

  1584   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 

  1584   produce any result by looping forever fetching @{term Nop}s in state @{text 0}. 

  1585   This solution implements essentially the definition in Chapter 3; it  

  1585   This solution implements essentially the definition in Chapter 3; it  

  1586   differs from the definition in Chapter 8, where perplexingly the instruction 

  1586   differs from the definition in Chapter 8, where perplexingly the instruction