DanilaFe/agda-spa
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Add a proof that edges lead to 'incoming' inclusion

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-09 16:56:45 -07:00
parent f0b0d51b48
commit b3a62da1fb
1 changed files with 7 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
Language.agda
View File

@ -10,6 +10,7 @@ open import Data.Fin using (Fin; suc; zero)
open import Data.Fin.Properties as FinProp using (suc-injective) open import Data.Fin.Properties as FinProp using (suc-injective)
open import Data.List as List using (List; []; _∷_) open import Data.List as List using (List; []; _∷_)
open import Data.List.Membership.Propositional as ListMem using () open import Data.List.Membership.Propositional as ListMem using ()
open import Data.List.Membership.Propositional.Properties as ListMemProp using (∈-filter⁺)
open import Data.List.Relation.Unary.All using (All; []; _∷_) open import Data.List.Relation.Unary.All using (All; []; _∷_)
open import Data.List.Relation.Unary.Any as RelAny using () open import Data.List.Relation.Unary.Any as RelAny using ()
open import Data.Nat using (ℕ; suc) open import Data.Nat using (ℕ; suc)
@ -100,3 +101,9 @@ record Program : Set where
incoming : State → List State incoming : State → List State
incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states incoming idx = List.filter (λ idx' → (idx' , idx) ∈? (Graph.edges graph)) states
edge⇒incoming : ∀ {s₁ s₂ : State} → (s₁ , s₂) ListMem.∈ (Graph.edges graph) →
s₁ ListMem.∈ (incoming s₂)
edge⇒incoming {s₁} {s₂} s₁,s₂∈es =
∈-filter⁺ (λ s' → (s' , s₂) ∈? (Graph.edges graph))
(states-complete s₁) s₁,s₂∈es