From: Tobias Nipkow <nipkow@in.tum.de>
András Z. Salamon and Michael Wehar have given us a large chunk of multitape
Turing machine theory in the form of these four entries:
https://isa-afp.org/entries/Multitape_TM_Substrate.html
https://isa-afp.org/entries/Multitape_Alphabet_Reduction.html
https://isa-afp.org/entries/Multitape_Alphabet_Enlargement.html
https://isa-afp.org/entries/Multitape_Alphabet_Roundtrip.html
If you ever wondered whether some TM construction in Hopcroft and Ullman really
works, look no further.
Enjoy!
Last updated: Sep 02 2026 at 16:10 UTC