Mercurial > hg > Members > kono > Proof > automaton
diff agda/sbconst2.agda @ 44:aa15eff1aeb3
seprate finite
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sat, 22 Dec 2018 11:45:37 +0900 |
| parents | cd311109d63b |
| children | f124fceba460 |
line wrap: on
line diff
--- a/agda/sbconst2.agda Sat Dec 22 03:08:21 2018 +0900 +++ b/agda/sbconst2.agda Sat Dec 22 11:45:37 2018 +0900 @@ -9,10 +9,11 @@ open import nfa open NAutomaton open Automaton +open import finiteSet open FiniteSet δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) -δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → nδ r i q ) +δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r ∧ nδ r i q ) subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )