fact: Definition tapeToList (t : tape) : list sig := match t with | niltape => [] | leftof s r => s :: r | rightof s l => List.rev (s :: l) | midtape l c r => (List.rev l) ++ [c] ++ r end.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM