64   step0 ("step") and

    64   step0 ("step") and

    65   tcontra ("contra") and

    65   tcontra ("contra") and

    66   code_tcontra ("code contra") and

    66   code_tcontra ("code contra") and

    67   steps0 ("steps") and

    67   steps0 ("steps") and

    68   exponent ("_\<^bsup>_\<^esup>") and

    68   exponent ("_\<^bsup>_\<^esup>") and

    70   tcopy ("copy") and 

    69   tcopy ("copy") and 

    71   tape_of ("\<langle>_\<rangle>") and 

    70   tape_of ("\<langle>_\<rangle>") and 

    72   tm_comp ("_ \<oplus> _") and 

    71   tm_comp ("_ \<oplus> _") and 

    73   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

    72   DUMMY  ("\<^raw:\mbox{$\_\!\_\,$}>") and

    74   inv_begin0 ("I\<^isub>0") and

    73   inv_begin0 ("I\<^isub>0") and

  1043   A program @{term p} started with a standard tape containing the (encoded) numbers

  1042   A program @{term p} started with a standard tape containing the (encoded) numbers

  1044   @{term ns} will \emph{halt} with a standard tape containing a single (encoded) 

  1043   @{term ns} will \emph{halt} with a standard tape containing a single (encoded) 

  1045   number is defined as

  1044   number is defined as

  1046 

  1045 

  1047   \begin{center}

  1046   \begin{center}

  1049   \end{center}

  1048   \end{center}

  1050 

  1049 

  1051   \noindent

  1050   \noindent

  1052   This roughly means we considering only Turing machine programs

  1051   This roughly means we considering only Turing machine programs

  1053   representing functions that take some numbers as input and produce a

  1052   representing functions that take some numbers as input and produce a