From 5f946de5e8f5fab65860c7592ec94efe54a32a75 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 10 May 2024 21:30:56 -0700 Subject: [PATCH] Remove last remaining assumption for correctness Signed-off-by: Danila Fedorin --- Analysis/Forward.agda | 2 -- Language.agda | 4 ++++ 2 files changed, 4 insertions(+), 2 deletions(-) diff --git a/Analysis/Forward.agda b/Analysis/Forward.agda index 678bccc..5d0458a 100644 --- a/Analysis/Forward.agda +++ b/Analysis/Forward.agda @@ -356,8 +356,6 @@ module WithProg (prog : Program) where in walkTrace ⟦joinForKey-s⟧ρ tr - postulate initialState-pred-∅ : incoming initialState ≡ [] - joinForKey-initialState-⊥ᵛ : joinForKey initialState result ≡ ⊥ᵛ joinForKey-initialState-⊥ᵛ = cong (λ ins → foldr _⊔ᵛ_ ⊥ᵛ (result [ ins ])) initialState-pred-∅ diff --git a/Language.agda b/Language.agda index 1c88ba8..5d54048 100644 --- a/Language.agda +++ b/Language.agda @@ -84,6 +84,10 @@ record Program : Set where incoming : State → List State incoming = predecessors graph + initialState-pred-∅ : incoming initialState ≡ [] + initialState-pred-∅ = + wrap-preds-∅ (buildCfg rootStmt) initialState (RelAny.here refl) + edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) → s₁ ListMem.∈ (incoming s₂) edge⇒incoming = edge⇒predecessor graph