stmts₁_trans — Mathlib

English

If q1 ∈ stmts₁(q2), then stmts₁(q1) ⊆ stmts₁(q2).

Русский

Если q1 ∈ stmts₁(q2), то stmts₁(q1) ⊆ stmts₁(q2).

LaTeX

$$$q_1 \in stmts_1(q_2) \Rightarrow stmts_1(q_1) \subseteq stmts_1(q_2)$$$

Lean4

theorem stmts₁_trans {q₁ q₂ : Stmt Γ Λ σ} : q₁ ∈ stmts₁ q₂ → stmts₁ q₁ ⊆ stmts₁ q₂ := by
  classical
  intro h₁₂ q₀ h₀₁
  induction q₂ with
    ( simp only [stmts₁] at h₁₂ ⊢
      simp only [Finset.mem_insert, Finset.mem_union, Finset.mem_singleton] at h₁₂)
  | branch p q₁ q₂ IH₁ IH₂ =>
    rcases h₁₂ with (rfl | h₁₂ | h₁₂)
    · unfold stmts₁ at h₀₁
      exact h₀₁
    · grind
    · grind
  | goto l => subst h₁₂; exact h₀₁
  | halt => subst h₁₂; exact h₀₁
  | _ _ q IH =>
    rcases h₁₂ with rfl | h₁₂
    · exact h₀₁
    · grind

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