English
stmts M S equals the insertNone of the union over q in S of stmts1(M(q)).
Русский
stmts M S равно insertNone( S ∪ ⋃_{q ∈ S} stmts1(M(q)) ).
LaTeX
$$$ stmts(M,S) = \operatorname{insertNone}\left( S \biUnion_{q\in S} stmts_1(M q) \right) $$$
Lean4
theorem step_supports (M : Λ → Stmt Γ Λ σ) {S : Finset Λ} (ss : Supports M S) :
∀ {c c' : Cfg Γ Λ σ}, c' ∈ step M c → c.l ∈ Finset.insertNone S → c'.l ∈ Finset.insertNone S
| ⟨some l₁, v, T⟩, c', h₁, h₂ =>
by
replace h₂ := ss.2 _ (Finset.some_mem_insertNone.1 h₂)
simp only [step, Option.mem_def, Option.some.injEq] at h₁; subst c'
revert h₂;
induction M l₁ generalizing v T with intro hs
| branch p q₁' q₂' IH₁ IH₂ =>
unfold stepAux; cases p v
· exact IH₂ _ _ hs.2
· exact IH₁ _ _ hs.1
| goto => exact Finset.some_mem_insertNone.2 (hs _)
| halt => apply Multiset.mem_cons_self
| load _ _ IH
| _ _ _ _ IH => exact IH _ _ hs
