51 predicate is either true or false because of the law of excluded

    51 predicate is either true or false because of the law of excluded

    52 middle. The only way to reason about computability in a classical

    52 middle. The only way to reason about computability in a classical

    53 theorem prover is to formalise a concrete model for computation.  We

    53 theorem prover is to formalise a concrete model for computation.  We

    54 formalise Turing machines and relate them to abacus machines and

    54 formalise Turing machines and relate them to abacus machines and

    55 recursive functions. We also formalise a universal Turing machine and

    55 recursive functions. We also formalise a universal Turing machine and

    57 programs. Our theory can be used to formalise other computability

    57 programs. Our theory can be used to formalise other computability

    58 results. We give one example about the computational equivalence of 

    58 results. We give one example about the computational equivalence of 

    59 single-sided Turing machines. 

    59 single-sided Turing machines. 

    60 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses

    60 %{\it we give one example about the undecidability of Wang's tiling problem, whose proof uses

    61 %the notion of a universal Turing machine.}

    61 %the notion of a universal Turing machine.}