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