toTM2Outputs — Mathlib

English

Forget the time bound: mapping a TM2OutputsInTime witness to a TM2Outputs witness by taking the underlying evaluation relation.

Русский

Убирая ограничение по времени, отображаем свидетельство TM2OutputsInTime в свидетельство TM2Outputs через базовое отношение эвалюации.

LaTeX

$$$$ \\mathrm{toTM2Outputs}(h) = h.\\mathrm{toEvalsTo}. $$$$

Lean4

/-- The forgetful map, forgetting the upper bound on the number of steps. -/
def toTM2Outputs {tm : FinTM2} {l : List (tm.Γ tm.k₀)} {l' : Option (List (tm.Γ tm.k₁))} {m : ℕ}
    (h : TM2OutputsInTime tm l l' m) : TM2Outputs tm l l' :=
  h.toEvalsTo

Похожие утверждения