fact: Definition tape_dir (t : tape sig) : option move := match t with | niltape _ => None | leftof _ _ => Some Lmove | midtape _ _ _ => Some Nmove | rightof _ _ => Some Rmove end.
imports: Undecidability.TM.Basic.Mono Undecidability.TM.Combinators.Combinators Undecidability.TM.Code.Code Undecidability.TM.Single.EncodeTapes Undecidability.TM.Compound(TMTac MoveToSymbol Multi Shift)