fact: Definition tape_local (t : tape sig) : list sig := match t with | niltape _ => [] | leftof a l => [] | rightof _ _ => [] | midtape _ a l => a :: l end.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM