fact: Definition GoToCurrent : pTM sigSim (option move) 1 := MoveToSymbol isMarked' id;; Switch ReadChar (fun (c : option sigSim) => Return Nop match c with | Some (inr (sigList_X (RightBlank true))) => Some Rmove | Some (inr (sigList_X (LeftBlank true))) => Some Lmove | Some (inr (sigList_X (MarkedSymbol _))) => Some Nmove | Some (inr (sigList_X NilBlank)) => None | _ => None 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)