English
Similarly, writing a list of booleans l to a statement q does not change its supports: SupportsStmt S (write l q) = SupportsStmt S q.
Русский
Аналогично, запись списка булевых значений l в инструкцию q не изменяет множества поддержек: SupportsStmt S (write l q) = SupportsStmt S q.
LaTeX
$$$\\operatorname{SupportsStmt}(S,\\ write(l,q)) = \\operatorname{SupportsStmt}(S,q).$$$
Lean4
theorem supportsStmt_write {S : Finset (Λ' Γ Λ σ)} {l : List Bool} {q : Stmt Bool (Λ' Γ Λ σ) σ} :
SupportsStmt S (write l q) = SupportsStmt S q := by induction l <;> simp only [write, SupportsStmt, *]