step_supports — Mathlib

English

In the TM0 setting, the transport of one-step reachability along tr holds similarly to the base setting.

Русский

В настройке 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_1},\\n Reaches_1 f_1 a_1 b_1 \\to \\exists b_2, tr b_1 b_2 \\wedge Reaches_1 f_2 a_2 b_2$$$

Lean4

theorem step_supports (M : Machine Γ Λ) {S : Set Λ} (ss : Supports M S) :
    ∀ {c c' : Cfg Γ Λ}, c' ∈ step M c → c.q ∈ S → c'.q ∈ S :=
  by
  intro ⟨q, T⟩ c' h₁ h₂
  rcases Option.map_eq_some_iff.1 h₁ with ⟨⟨q', a⟩, h, rfl⟩
  exact ss.2 h h₂

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