tr_eval_dom — Mathlib

English

The domain of evaluation after translation equals the domain of evaluation of the original machine: Eval on tr M equals Eval on M under dom equality.

Русский

Область определения вычисления после перевода совпадает с областью определения вычисления исходной машины.

LaTeX

$$$ (TM1.eval (tr M) (trInit k L)).Dom \iff (TM2.eval M k L).Dom $$$

Lean4

theorem tr_eval_dom (k) (L : List (Γ k)) : (TM1.eval (tr M) (trInit k L)).Dom ↔ (TM2.eval M k L).Dom :=
  Turing.tr_eval_dom (tr_respects M) (trCfg_init k L)

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