Emitting the complete halted output

After source halting, the simulator emits one bit per step and halts at the first blank. Together with initialization and source simulation, this costs at most 2 * input.length + sourceTime + output.length + 4 steps.

structure Complexity.MathlibTM0.Emitting (M : BinaryMachine) {input : List Bool} (tape : Turing.Tape M.Alphabet) (emitted : List Bool) (d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input) : Prop

The simulator is emitting from the represented tape, after previously emitted bits.

• state : d.state = some Control.emit

  The simulator is in its output phase.

• output : d.output = emitted

  The output emitted so far.

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

  The tracks represent the remaining tape relative to their heads.

theorem Complexity.MathlibTM0.Sim.halt {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) (hh : Turing.TM0.step M.code c = none) : Emitting M c.Tape [] (Turing.MultiTapeTM.step d)

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

theorem Complexity.MathlibTM0.Emitting.step_bit {M : BinaryMachine} {input : List Bool} {tape : Turing.Tape M.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input} (h : Emitting M tape emitted d) {b : Bool} (hb : tape.head = M.bit b) : Emitting M (Turing.Tape.move Turing.Dir.right tape) (emitted ++ [b]) (Turing.MultiTapeTM.step d)

theorem Complexity.MathlibTM0.Emitting.step_blank {M : BinaryMachine} {input : List Bool} {tape : Turing.Tape M.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input} (h : Emitting M tape emitted d) (hb : tape.head = default) : (Turing.MultiTapeTM.step d).state = none ∧ (Turing.MultiTapeTM.step d).output = emitted

theorem Complexity.MathlibTM0.Emitting.run {M : BinaryMachine} {input : List Bool} (output : List Bool) {tape : Turing.Tape M.Alphabet} {emitted : List Bool} {d : Turing.Cfg (Fintype.card M.Alphabet) Bool (Control M.State) input} (h : Emitting M tape emitted d) (ho : ∀ (j : ℕ), tape.nth ↑j = (List.map M.bit output).getI j) : (Turing.MultiTapeTM.runFrom d (output.length + 1)).state = none ∧ (Turing.MultiTapeTM.runFrom d (output.length + 1)).output = emitted ++ output

theorem Complexity.MathlibTM0.computes_proof (M : BinaryMachine) {input output : List Bool} {time : ℕ} (h : M.OutputsWithin input output time) : (machine M).ComputesInTimeAndSpace input output (2 * input.length + time + output.length + 4) (Turing.MultiTapeTM.spaceUsed (Turing.MultiTapeTM.initCfg input) (2 * input.length + time + output.length + 4))