fact: Definition mirror_tape (t : tape sig) : tape sig := match t with | niltape _ => niltape _ | leftof r rs => rightof r rs | rightof l ls => leftof l ls | midtape ls m rs => midtape rs m ls end.
imports: Undecidability.Shared.Libs.PSL.Vectors.Vectors Undecidability.TM.TM