English
A formal claim that a TM2 machine outputs l' when given l within m steps is modeled by a predicate TM2OutputsInTime tm l l' m, defined as an evaluation relation with a halt condition mapped to l'.
Русский
Утверждение о том, что машина TM2 выдает l' при входе l за не более m шагов, моделируется предикатом TM2OutputsInTime tm l l' m, определяемым через отношение эвалюаций и соответствующее завершение.
LaTeX
$$$$ \\text{TM2OutputsInTime}(tm, l, l', m) \\ ;\\; \\text{равно} \\; EvalsToInTime\\; tm.step\\ (initList\\ tm\\ l)\\ ((\\text{Option.map} (\\text{haltList } tm)) l')\\ m. $$$$
Lean4
/-- A proof of tm outputting l' when given l in at most m steps. -/
def TM2OutputsInTime (tm : FinTM2) (l : List (tm.Γ tm.k₀)) (l' : Option (List (tm.Γ tm.k₁))) (m : ℕ) :=
EvalsToInTime tm.step (initList tm l) ((Option.map (haltList tm)) l') m
