English
For each c and v, the evaluation of the encoded code under the machine semantics corresponds to evaluating c on v in the Partrec-to-TM2 translation, i.e., the evaluation result equals the mapped halt code applied to v.
Русский
Пусть дано c и v; эвалюация закодированного кода под машинной семантикой соответствует вычислению c на v в трансляции Partrec-to-TM2; результат равен mаппированномуhalt-коду, применённому к v.
LaTeX
$$$\forall (c:Code)(v:\,\mathrm{List}\;\mathbb{N}),\; \operatorname{eval}(\mathrm{TM2.step}\;\mathrm{tr})(\operatorname{init}(c,v)) = \mathrm{halt} \langle\text{?},\;\,\cdots \rangle$$$
Lean4
theorem tr_eval (c v) : eval (TM2.step tr) (init c v) = halt <$> Code.eval c v :=
by
obtain ⟨i, h₁, h₂⟩ := tr_init c v
refine Part.ext fun x => ?_
rw [reaches_eval h₂.to_reflTransGen]; simp only [Part.map_eq_map, Part.mem_map_iff]
refine ⟨fun h => ?_, ?_⟩
· obtain ⟨c, hc₁, hc₂⟩ := tr_eval_rev tr_respects h₁ h
simp [stepNormal_eval] at hc₂
obtain ⟨v', hv, rfl⟩ := hc₂
exact ⟨_, hv, hc₁.symm⟩
· rintro ⟨v', hv, rfl⟩
have := Turing.tr_eval (b₁ := Cfg.halt v') tr_respects h₁
simp only [stepNormal_eval, Part.map_eq_map, Part.mem_map_iff, Cfg.halt.injEq, exists_eq_right] at this
obtain ⟨_, ⟨⟩, h⟩ := this hv
exact h
