Add proof about setVariablesForState

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-08 22:09:56 -07:00
parent 7fe46b014c
commit 4350919871

View File

@ -234,3 +234,6 @@ module WithProg (prog : Program) where
updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ updateVariablesFromStmt-fold-matches [] ⟦vs⟧ρ = ⟦vs⟧ρ
updateVariablesFromStmt-fold-matches {bs bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ρ,bss'⇒ρ₂) ⟦vs⟧ρ = updateVariablesFromStmt-fold-matches {bs bss'} {vs} {ρ₁} {ρ₂} (ρ₁,bs⇒ρ ρ,bss'⇒ρ₂) ⟦vs⟧ρ =
updateVariablesFromStmt-fold-matches {bss'} {updateVariablesFromStmt bs vs} ρ,bss'⇒ρ₂ (updateVariablesFromStmt-matches ρ₁,bs⇒ρ ⟦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