fact: Definition DoWrite (d : option move) (s : sig) : pTM sigSim unit 1 := match d with | Some Lmove => Shift_L (fun _ => false) (inl UNKNOWN);; MoveToSymbol isReturnMarker id;; WriteMove (inr (sigList_X (MarkedSymbol s))) Lmove;; WriteMove (inr (sigList_X (LeftBlank false))) Rmove | Some Rmove => Shift (fun _ => false) (inl UNKNOWN);; MoveToSymbol_L isReturnMarker id;; WriteMove (inr (sigList_X (MarkedSymbol s))) Rmove;; WriteMove (inr (sigList_X (RightBlank false))) Lmove | Some Nmove => Write (inr (sigList_X (MarkedSymbol s))) | None => Shift (fun _ => false) (inl UNKNOWN);; MoveToSymbol_L isReturnMarker id;; Shift_L (fun _ => false) (inr (sigList_X (MarkedSymbol s)));; MoveToSymbol isReturnMarker id;; WriteMove (inr (sigList_X (LeftBlank false))) Rmove;; Move Rmove;; WriteMove (inr (sigList_X (RightBlank false))) Lmove 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)