Source-step simulation on binary tracks

All work heads move together. Their contents at each relative offset encode the source tape at that offset, so each source write or move takes one CSLib step.

structure Complexity.MathlibTM0.Sim (M : BinaryMachine) {input : List Bool} (c : M.Config) (d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input) : Prop

The simulator is executing the source state with the same relative tape contents.

• state : d.state = some (Control.run c.q)

  The source and simulator controls agree.

• output : d.output = []

  Output emission has not started.

• tape (i : Fin (Fintype.card M.Alphabet)) (z : ℤ) : d.workTapes i (d.workTapePos i + z) = SymbolTracks.encode (c.Tape.nth z) ((trackEquiv M) i)

  Every track agrees at every offset from its head.

theorem Complexity.MathlibTM0.Sim.read {M : BinaryMachine} {input : List Bool} {c : M.Config} {d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input} (h : Sim M c d) : (SymbolTracks.decode fun (a : M.Alphabet) => d.workTapeSymbols ((trackEquiv M).symm a)) = c.Tape.head

theorem Complexity.MathlibTM0.move_nth {Γ : Type u_1} [Inhabited Γ] (dir : Turing.Dir) (t : Turing.Tape Γ) (z : ℤ) : (Turing.Tape.move dir t).nth z = t.nth (z + ↑(moveSign dir))

theorem Complexity.MathlibTM0.Sim.step {M : BinaryMachine} {input : List Bool} {c c' : M.Config} {d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input} (h : Sim M c d) (hs : Turing.TM0.step M.code c = some c') : Sim M c' (Turing.MultiTapeTM.step d)

theorem Complexity.MathlibTM0.Sim.run {M : BinaryMachine} {input : List Bool} {c c' : M.Config} {d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input} (h : Sim M c d) (t : ℕ) (hs : M.run t c = some c') : Sim M c' (Turing.MultiTapeTM.runFrom d t)