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