stmts₁_supportsStmt_mono — Mathlib

English

If q1 ∈ stmts1(q2) and S supports q2, then S supports q1.

Русский

Если q1 ∈ stmts1(q2) и S поддерживает q2, то S поддерживает q1.

LaTeX

$$$ q_1 \in stmts_1(q_2) \land 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 f 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
  | load _ _ IH
  | _ _ _ _ IH => rcases h with (rfl | h) <;> [exact hs; exact IH h hs]

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