Copying and rewinding the source input

Initialization uses exactly 2 * input.length + 2 CSLib transitions. Each source alphabet track contains the input symbol's encoding at every position.

theorem Complexity.MathlibTM0.nth_mk₁ {Γ : Type u_1} [Inhabited Γ] (l : List Γ) (z : ℤ) : (Turing.Tape.mk₁ l).nth z = if z < 0 then default else l.getI z.toNat

theorem Complexity.MathlibTM0.nth_mk₁_append_singleton {Γ : Type u_1} [Inhabited Γ] (l : List Γ) (a : Γ) (z : ℤ) : (Turing.Tape.mk₁ (l ++ [a])).nth z = if z = ↑l.length then a else (Turing.Tape.mk₁ l).nth z

noncomputable def Complexity.MathlibTM0.inputContents (M : BinaryMachine) (bits : List Bool) (i : Track M) (z : ℤ) : Option Bool

The track contents after copying the specified input prefix.

Equations

• Complexity.MathlibTM0.inputContents M bits i z = Complexity.SymbolTracks.encode ((Turing.Tape.mk₁ (List.map M.bit bits)).nth z) ((Complexity.MathlibTM0.trackEquiv M) i)

theorem Complexity.MathlibTM0.inputContents_nil (M : BinaryMachine) : inputContents M [] = fun (x : Track M) (x_1 : ℤ) => none

theorem Complexity.MathlibTM0.inputContents_append (M : BinaryMachine) (bits : List Bool) (b : Bool) (i : Track M) : inputContents M (bits ++ [b]) i = Function.update (inputContents M bits i) (↑bits.length) (SymbolTracks.encode (M.bit b) ((trackEquiv M) i))

noncomputable def Complexity.MathlibTM0.copyCfg (M : BinaryMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) w

The configuration after copying an input prefix of length t.

Equations

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

noncomputable def Complexity.MathlibTM0.rewindCfg (M : BinaryMachine) (w : List Bool) (t : ℕ) (ht : t ≤ w.length) : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) w

The configuration with t copied input cells left to rewind.

Equations

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

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

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

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

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

theorem Complexity.MathlibTM0.runFrom_add (M : BinaryMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) w) (t u : ℕ) : Turing.MultiTapeTM.runFrom d (t + u) = Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.runFrom d t) u

theorem Complexity.MathlibTM0.runFrom_succ (M : BinaryMachine) {w : List Bool} (d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) w) (t : ℕ) : Turing.MultiTapeTM.runFrom d (t + 1) = Turing.MultiTapeTM.step (Turing.MultiTapeTM.runFrom d t)

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

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

theorem Complexity.MathlibTM0.rewindCfg_zero_sim (M : BinaryMachine) (w : List Bool) : Sim M (Turing.TM0.init (List.map M.bit w)) (Turing.MultiTapeTM.step (rewindCfg M w 0 ⋯))

theorem Complexity.MathlibTM0.init_sim (M : BinaryMachine) (w : List Bool) : Sim M (Turing.TM0.init (List.map M.bit w)) (Turing.MultiTapeTM.runFrom (Turing.MultiTapeTM.initCfg w) (2 * w.length + 2))