The first halt and the computed output

A time bound gives a step at which the run first halts, and the output at that step is the computed output.

Main results

• Turing.MultiTapeTM.exists_haltsAt_of_runsInTime: the first halt is no later than the time bound.
• Turing.MultiTapeTM.output_haltsAt: the output at the first halt is the computed output.

theorem Turing.MultiTapeTM.output_haltsAt {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input output : List Symbol} {h : ℕ} (hc : tm.Computes input output) (hh : tm.HaltsAt (tm.initCfg input) h) : (runFrom (tm.initCfg input) h).output = output

The output at the first halt is the computed output.

theorem Turing.MultiTapeTM.exists_haltsAt_of_runsInTime {k : ℕ} {State : Type u_1} {Symbol : Type u_2} {tm : MultiTapeTM k Symbol State} {input : List Symbol} {t : ℕ} (ht : tm.RunsInTime input t) : ∃ h ≤ t, tm.HaltsAt (tm.initCfg input) h

The first halt is no later than the time bound.