A machine that marks the cell left of its head

markWork Symbol write is a machine with one work tape that writes write to the cell left of its head and moves the head back, halting after two steps. It neither moves the input head nor emits output. To use it on tape i of a machine with more tapes, embed it with Turing.MultiTapeTM.tapeEmb.

inductive Turing.MultiTapeTM.MarkWorkState : Type

The states of markWork: start steps left, put writes and steps back.

• start : MarkWorkState
• put : MarkWorkState

@[instance_reducible]

instance Turing.MultiTapeTM.instDecidableEqMarkWorkState : DecidableEq MarkWorkState

@[instance_reducible]

instance Turing.MultiTapeTM.instFintypeMarkWorkState : Fintype MarkWorkState

def Turing.MultiTapeTM.markWork (Symbol : Type u_2) (write : Option Symbol) : MultiTapeTM 1 Symbol MarkWorkState

markWork Symbol write steps left, writes write (erasing if write = none), steps back right and halts.

theorem Turing.MultiTapeTM.runFrom_markWork {Symbol : Type u_1} {input : List Symbol} (write : Option Symbol) (ip : Fin (input.length + 2)) (tp : ℤ → Option Symbol) (out : List Symbol) (p : ℤ) : runFrom { state := some (markWork Symbol write).q₀, inputPos := ip, workTapes := fun (x : Fin 1) => tp, workTapePos := fun (x : Fin 1) => p, output := out } 2 = { state := none, inputPos := ip, workTapes := fun (x : Fin 1) => Function.update tp (p - 1) write, workTapePos := fun (x : Fin 1) => p, output := out }

Started with its head at p, after two steps markWork Symbol write has halted with write at cell p - 1 and its head back at p.