English
For any finite set S of labels Λ, any StAct s and TM2.Stmt q, the statement that stRun(s,q) is supported by S is equivalent to q being supported by S. In other words, running the step s over q does not change the S-support property.
Русский
Для любого конечного множества S меток Λ, для любой операции StAct s и команды TM2.Stmt q утверждение, что stRun(s,q) поддерживается S, эквивалентно тому, что q поддерживается S. Другими словами, выполнение шага s над q не меняет свойство поддержки S.
LaTeX
$$$\operatorname{SupportsStmt}(S, \operatorname{stRun}(s,q)) \iff \operatorname{SupportsStmt}(S,q)$$$
Lean4
theorem supports_run (S : Finset Λ) {k : K} (s : StAct K Γ σ k) (q : TM2.Stmt Γ Λ σ) :
TM2.SupportsStmt S (stRun s q) ↔ TM2.SupportsStmt S q := by cases s <;> rfl
