A formalization of multi-tape Turing machines