contSupp_cons₁ — Mathlib

English

The contSupp for Cont'.cons₂ k equals trStmts₁ (head stack ⟨Λ'.ret k⟩) ∪ contSupp k.

Русский

Cont'.cons₂ k имеет contSupp = trStmts₁ (head stack ⟨Λ'.ret k⟩) ∪ contSupp k.

LaTeX

$$$\forall k\; contSupp (Cont'.cons₂ k) = trStmts₁ (head stack <| Λ'.ret k) \cup contSupp k$$$

Lean4

@[simp]
theorem contSupp_cons₁ (fs k) :
    contSupp (Cont'.cons₁ fs k) =
      trStmts₁
          (move₂ (fun _ => false) main aux <|
            move₂ (fun s => s = Γ'.consₗ) stack main <|
              move₂ (fun _ => false) aux stack <| trNormal fs (Cont'.cons₂ k)) ∪
        codeSupp fs (Cont'.cons₂ k) :=
  by simp [codeSupp, contSupp]

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