Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/sbconst2.agda @ 411:207e6c4e155c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 Nov 2023 17:40:55 +0900 |
| parents | a60132983557 |
| children |
line wrap: on
line diff
--- a/automaton-in-agda/src/sbconst2.agda Wed Nov 22 17:07:01 2023 +0900 +++ b/automaton-in-agda/src/sbconst2.agda Wed Nov 29 17:40:55 2023 +0900 @@ -20,7 +20,8 @@ --- ( Q → Σ → Q → Bool ) transition of NFA --- (Q → Bool) → Σ → (Q → Bool) generate transition of Automaton -δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) +δconv : { Q : Set } { Σ : Set } → (exists :( Q → Bool ) → Bool ) → (nδ : Q → Σ → Q → Bool ) + → (Q → Bool) → Σ → (Q → Bool) δconv {Q} { Σ} exists nδ f i q = exists ( λ r → f r /\ nδ r i q ) subset-construction : { Q : Set } { Σ : Set } →