stmts₁_supportsStmt_mono — Mathlib

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]

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