fact: Definition tape_move (t : tape) (m : move) := match m with | Rmove => tape_move_right t | Lmove => tape_move_left t | Nmove => t end.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM