1320 

  1320 

  1321   \noindent

  1321   \noindent

  1322   which means that if the recursive function @{text r} with arguments @{text ns} evaluates

  1322   which means that if the recursive function @{text r} with arguments @{text ns} evaluates

  1323   to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started

  1323   to @{text n}, then the corresponding Turing machine @{term "tm_of_rec r"} if started

  1324   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate

  1324   with the standard tape @{term "([Bk, Bk], <ns::nat list>)"} will terminate

  1326 

  1326 

  1327   and the also the definition of the

  1327   and the also the definition of the

  1328   universal function (we refer the reader to our formalisation).

  1328   universal function (we refer the reader to our formalisation).

  1329   

  1329   

  1330 *}

  1330 *}