English
For any finite set S of instructions and any statement q, applying a move operation to q does not change which statements S supports: SupportsStmt S (move n d q) = SupportsStmt S q.
Русский
Для любого конечного множества S инструкций и любой инструкции q выполнение перемещения move n d над q не изменяет набор поддержек: SupportsStmt S (move n d q) = SupportsStmt S q.
LaTeX
$$$\\operatorname{SupportsStmt}(S,\\ \\operatorname{move}(n,d,q)) = \\operatorname{SupportsStmt}(S,q).$$$
Lean4
theorem supportsStmt_move {S : Finset (Λ' Γ Λ σ)} {d : Dir} {q : Stmt Bool (Λ' Γ Λ σ) σ} :
SupportsStmt S (move n d q) = SupportsStmt S q :=
by
suffices ∀ {i}, SupportsStmt S ((Stmt.move d)^[i] q) = _ from this
intro i; induction i generalizing q <;> simp only [*, iterate]; rfl
