English
There exist a state-encoding S and a bottom-list L' such that addBottom L' equals L1 and the mapped projections of L' match the reversed map of S and S k equals L2.
Русский
Существуют код состояния S и список L' такие, что addBottom L' = L1 и отображение проекции L' совпадает с обращенным списком S, а S k = L2.
LaTeX
$$∃ S, L' : (∀ k, List (Γ k)),\; addBottom L' = L1 ∧ (∀ k, L'.map (proj k) = ListBlank.mk ((S k).map some).reverse) ∧ S k = L2$$
Lean4
theorem tr_eval (k) (L : List (Γ k)) {L₁ L₂} (H₁ : L₁ ∈ TM1.eval (tr M) (trInit k L)) (H₂ : L₂ ∈ TM2.eval M k L) :
∃ (S : ∀ k, List (Γ k)) (L' : ListBlank (∀ k, Option (Γ k))),
addBottom L' = L₁ ∧ (∀ k, L'.map (proj k) = ListBlank.mk ((S k).map some).reverse) ∧ S k = L₂ :=
by
obtain ⟨c₁, h₁, rfl⟩ := (Part.mem_map_iff _).1 H₁
obtain ⟨c₂, h₂, rfl⟩ := (Part.mem_map_iff _).1 H₂
obtain ⟨_, ⟨L', hT⟩, h₃⟩ := Turing.tr_eval (tr_respects M) (trCfg_init k L) h₂
cases Part.mem_unique h₁ h₃
exact ⟨_, L', by simp only [Tape.mk'_right₀], hT, rfl⟩
