fact: Definition DoMove (d : option move) (m : move) : pTM sigSim unit 1 := match d with | Some Lmove => match m with | Nmove => Nop | Lmove => Nop | Rmove => ToggleMarked;; Move Rmove;; ToggleMarked end | Some Rmove => match m with | Nmove => Nop | Rmove => Nop | Lmove => ToggleMarked;; Move Lmove;; ToggleMarked end | Some Nmove => match m with | Nmove => Nop | Rmove => ToggleMarked;; Move Rmove;; ToggleMarked | Lmove => ToggleMarked;; Move Lmove;; ToggleMarked end | None => Nop 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)