Copying a first-cell-marked input

The copier distinguishes the first input bit, writes the empty-input marker when necessary, and then uses the existing simulator's rewind phase. The total initialization cost remains exactly 2 * input.length + 2 transitions.

def Complexity.MathlibTM0.MarkedMachine.prefixCells (M : MarkedMachine) : List Bool → List M.Alphabet

Cells copied before the end of input is encountered.

Equations

• M.prefixCells [] = []
• M.prefixCells (b :: bs) = M.bit true b :: List.map (M.bit false) bs

theorem Complexity.MathlibTM0.MarkedMachine.prefixCells_length (M : MarkedMachine) (w : List Bool) : (M.prefixCells w).length = w.length

theorem Complexity.MathlibTM0.MarkedMachine.prefixCells_append (M : MarkedMachine) (w : List Bool) (b : Bool) : M.prefixCells (w ++ [b]) = M.prefixCells w ++ [M.bit w.isEmpty b]

theorem Complexity.MathlibTM0.MarkedMachine.inputCells_false (M : MarkedMachine) (w : List Bool) : M.inputCells false w = List.map (M.bit false) w

theorem Complexity.MathlibTM0.MarkedMachine.inputCells_true (M : MarkedMachine) (w : List Bool) : M.inputCells true w = if w.isEmpty = true then [M.empty] else M.prefixCells w

noncomputable def Complexity.MathlibTM0.MarkedMachine.contents (M : MarkedMachine) (cells : List M.Alphabet) (i : Track M.binary) (z : ℤ) : Option Bool

Symbol tracks containing the specified complete source cells.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.MathlibTM0.MarkedMachine.contents_nil (M : MarkedMachine) : M.contents [] = fun (x : Track M.binary) (x_1 : ℤ) => none

theorem Complexity.MathlibTM0.MarkedMachine.contents_append (M : MarkedMachine) (cells : List M.Alphabet) (a : M.Alphabet) (i : Track M.binary) : M.contents (cells ++ [a]) i = Function.update (M.contents cells i) (↑cells.length) (SymbolTracks.encode (Symbol.source a) ((trackEquiv M.binary) i))

noncomputable def Complexity.MathlibTM0.MarkedMachine.copyCfg (M : MarkedMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool M.TargetState w

The marked copier after reading the first t input bits.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Complexity.MathlibTM0.MarkedMachine.rewindCfg (M : MarkedMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool M.TargetState w

A rewind configuration with the complete marked input already on the tracks.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.MathlibTM0.MarkedMachine.copyCfg_zero (M : MarkedMachine) (w : List Bool) : M.copyCfg w 0 ⋯ = Turing.MultiTapeTM.initCfg w

theorem Complexity.MathlibTM0.MarkedMachine.copyCfg_step (M : MarkedMachine) (w : List Bool) (t : ℕ) (ht : t < w.length) : Turing.MultiTapeTM.step (M.copyCfg w t ⋯) = M.copyCfg w (t + 1) ⋯

theorem Complexity.MathlibTM0.MarkedMachine.copyCfg_end (M : MarkedMachine) (w : List Bool) : Turing.MultiTapeTM.step (M.copyCfg w w.length ⋯) = M.rewindCfg w w.length ⋯

theorem Complexity.MathlibTM0.MarkedMachine.rewindCfg_step (M : MarkedMachine) (w : List Bool) (t : ℕ) (ht : t + 1 ≤ w.length) : Turing.MultiTapeTM.step (M.rewindCfg w (t + 1) ht) = M.rewindCfg w t ⋯

theorem Complexity.MathlibTM0.MarkedMachine.run_add (M : MarkedMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool M.TargetState w) (t u : ℕ) : Turing.MultiTapeTM.runFrom d (t + u) = Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.runFrom d t) u

theorem Complexity.MathlibTM0.MarkedMachine.run_succ (M : MarkedMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool M.TargetState w) (t : ℕ) : Turing.MultiTapeTM.runFrom d (t + 1) = Turing.MultiTapeTM.step (Turing.MultiTapeTM.runFrom d t)

theorem Complexity.MathlibTM0.MarkedMachine.run_copy (M : MarkedMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) t = M.copyCfg w t ht

theorem Complexity.MathlibTM0.MarkedMachine.run_rewind (M : MarkedMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.MultiTapeTM.runFrom (M.rewindCfg w t ht) t = M.rewindCfg w 0 ⋯

noncomputable def Complexity.MathlibTM0.MarkedMachine.readyCfg (M : MarkedMachine) (w : List Bool) : Turing.Cfg (Fintype.card M.binary.Alphabet) Bool (Control M.State) w

The legacy simulator configuration at the start of source execution.

Equations

• One or more equations did not get rendered due to their size.

theorem Complexity.MathlibTM0.MarkedMachine.ready_sim (M : MarkedMachine) (w : List Bool) : Sim M.binary (M.sourceCfg (Turing.TM0.init (M.inputCells true w))) (M.readyCfg w)

theorem Complexity.MathlibTM0.MarkedMachine.rewindCfg_zero (M : MarkedMachine) (w : List Bool) : Turing.MultiTapeTM.step (M.rewindCfg w 0 ⋯) = M.liftCfg (M.readyCfg w)

theorem Complexity.MathlibTM0.MarkedMachine.init_ready (M : MarkedMachine) (w : List Bool) : Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (2 * w.length + 2) = M.liftCfg (M.readyCfg w)