English
There exists a result state b such that the execution starting from init c v, i.e., the initial configuration produced by evaluating c on v, is reachable by repeatedly taking a normal-step configuration step; i.e., there is a trace to b.
Русский
Существует состояние b, к которому приводится исполнение, начинающееся с инициализации init c v, то есть с начальной конфигурацией, полученной при выполнении c на v; существует след, ведущий к b.
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
/-- The initial state, evaluating function `c` on input `v`. -/
def init (c : Code) (v : List ℕ) : Cfg' :=
⟨some (trNormal c Cont'.halt), none, K'.elim (trList v) [] [] []⟩
