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