148 recursive functions to abacus machines, the textbook again only shows

   148 recursive functions to abacus machines, the textbook again only shows

   149 how it can be done for 2- and 3-ary functions, but in the

   149 how it can be done for 2- and 3-ary functions, but in the

   150 formalisation we need arbitrary functions. But the general ideas for

   150 formalisation we need arbitrary functions. But the general ideas for

   151 how to do this are clear enough in \cite{Boolos87}. However, one

   151 how to do this are clear enough in \cite{Boolos87}. However, one

   152 aspect that is completely left out from the informal description in

   152 aspect that is completely left out from the informal description in

   154 machines are correct. We will introduce Hoare-style proof rules

   154 machines are correct. We will introduce Hoare-style proof rules

   155 which help us with such correctness arguments of Turing machines.

   155 which help us with such correctness arguments of Turing machines.

   156 

   156 

   157 The main difference between our formalisation and the one by Asperti

   157 The main difference between our formalisation and the one by Asperti

   158 and Ricciotti is that their universal Turing machine uses a different

   158 and Ricciotti is that their universal Turing machine uses a different