supportsStmt_write — Mathlib

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, *]

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