fact: Definition tape_move_right := fun (t : tape) => match t with | niltape => niltape | rightof _ _ =>t | leftof a rs =>midtape [ ] a rs | midtape ls a rs => tape_move_right' ls a rs end.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM