English
In the TM0 setting, the reverse transport of reachability across tr holds with a witness.
Русский
В настройке TM0 обратный перенос достижимости по отношению tr имеет свидетеля.
LaTeX
$$$\\forall {\\alpha,\\beta, f_1, f_2, tr},\\n (H : Respects f_1 f_2 tr) \\to \\forall {a_1 a_2},\\n tr\\ a_1 a_2 \\to \\forall {b_2},\\n Reaches f_2 a_2 b_2 \\to \\exists c_1 c_2, Reaches f_2 b_2 c_2 \\wedge tr c_1 c_2 \\wedge Reaches f_1 a_1 c_1$$$
Lean4
theorem map_step {S : Set Λ} (f₂₁ : Function.RightInverse f₁ f₂) (g₂₁ : ∀ q ∈ S, g₂ (g₁ q) = q) :
∀ c : Cfg Γ Λ, c.q ∈ S → (step M c).map (Cfg.map f₁ g₁) = step (M.map f₁ f₂ g₁ g₂) (Cfg.map f₁ g₁ c)
| ⟨q, T⟩, h => by
unfold step Machine.map Cfg.map
simp only [Turing.Tape.map_fst, g₂₁ q h, f₂₁ _]
rcases M q T.1 with (_ | ⟨q', d | a⟩); · rfl
· simp only [Option.map_some, Tape.map_move f₁]
rfl
· simp only [Option.map_some, Tape.map_write]
rfl
