tr_init — Mathlib

English

There exists b such that the normal-step from c with halt continuation yields b, and the initial configuration init c v is reachable to b in one TM2 step from tr.

Русский

Существует b, такой что нормальный шаг от кода c с остановленным продолжением ведет к b, а конфигурация init c v достижима из начального состояния за один шаг TM2.step.

LaTeX

$$$\exists b\,\big(\operatorname{TrCfg}(\operatorname{stepNormal}(c,Cont.halt,v),b) \land \operatorname{Reaches}_1(\mathrm{TM2.step}\;\mathrm{tr})\; (\operatorname{init}(c,v))\ b\big)$$$

Lean4

theorem tr_init (c v) : ∃ b, TrCfg (stepNormal c Cont.halt v) b ∧ Reaches₁ (TM2.step tr) (init c v) b :=
  trNormal_respects _ _ _ _

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