English
If q1 ∈ stmts₁(q2) and S supports q₂, then S supports q₁.
Русский
Если q₁ ∈ stmts₁(q₂) и S поддерживает q₂, то S поддерживает q₁.
LaTeX
$$$q_1 \in stmts_1(q_2) \wedge SupportsStmt S q_2 \Rightarrow SupportsStmt S q_1$$$
Lean4
theorem stmts₁_supportsStmt_mono {S : Finset Λ} {q₁ q₂ : Stmt Γ Λ σ} (h : q₁ ∈ stmts₁ q₂) (hs : SupportsStmt S q₂) :
SupportsStmt S q₁ := by
induction q₂ with simp only [stmts₁, SupportsStmt, Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h hs
| branch p q₁ q₂ IH₁ IH₂ => rcases h with (rfl | h | h); exacts [hs, IH₁ h hs.1, IH₂ h hs.2]
| goto l => subst h; exact hs
| halt => subst h; trivial
| _ _ q IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]