fact: Definition encode_tape (sig : Type) (t : tape sig) : list (sigTape sig) := match t with | niltape _ => [NilBlank] | leftof r rs => LeftBlank true :: UnmarkedSymbol r :: map UnmarkedSymbol rs ++ [RightBlank false] | midtape ls m rs => LeftBlank false :: map UnmarkedSymbol (rev ls) ++ MarkedSymbol m :: map UnmarkedSymbol rs ++ [RightBlank false] | rightof l ls => LeftBlank false :: map UnmarkedSymbol (rev ls) ++ [UnmarkedSymbol l; RightBlank true] end.
imports: Undecidability.TM.Compound.TMTac Undecidability.TM.Code.Code Undecidability.TM.Basic.Mono Undecidability.TM.Compound.Multi