From 435091987152ced619f27fcc75476541a2f93fa5 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Wed, 8 May 2024 22:09:56 -0700 Subject: [PATCH] Add proof about setVariablesForState Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 3 +++ 1 file changed, 3 insertions(+) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index c2f4d2d..270a4d8 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -234,3 +234,6 @@ module WithProg (prog : Program) where updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ updateVariablesFromStmt-fold-matches {bs ∷ bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ∷ ρ,bss'⇒ρ₂) ⟦vs⟧ρ₁ = updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦vs⟧ρ₁) + + updateVariablesForState-matches : ∀ {s sv ρ₁ ρ₂} → ρ₁ , (code s) ⇒ᵇˢ ρ₂ → ⟦ variablesAt s sv ⟧ᵛ ρ₁ → ⟦ updateVariablesForState s sv ⟧ᵛ ρ₂ + updateVariablesForState-matches = updateVariablesFromStmt-fold-matches