English
If q1 is in stmts1(q2), then stmts1(q1) is contained in stmts1(q2).
Русский
Если q1 ∈ stmts1(q2), то stmts1(q1) ⊆ stmts1(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_singleton, Finset.mem_union] at h₁₂)
| branch f q₁ q₂ IH₁ IH₂ =>
rcases h₁₂ with (rfl | h₁₂ | h₁₂)
· unfold stmts₁ at h₀₁
exact h₀₁
· exact Finset.mem_insert_of_mem (Finset.mem_union_left _ (IH₁ h₁₂))
· exact Finset.mem_insert_of_mem (Finset.mem_union_right _ (IH₂ h₁₂))
| goto l => subst h₁₂; exact h₀₁
| halt => subst h₁₂; exact h₀₁
| load _ q IH
| _ _ _ q IH =>
rcases h₁₂ with (rfl | h₁₂)
· unfold stmts₁ at h₀₁
exact h₀₁
· exact Finset.mem_insert_of_mem (IH h₁₂)
