Mercurial > hg > Members > kono > Proof > automaton
comparison automaton-in-agda/src/derive.agda @ 330:407684f806e4
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 16 Nov 2022 17:43:10 +0900 |
| parents | 1c8ed1220489 |
| children | ce4e44cee2d3 |
comparison
equal
deleted
inserted
replaced
| 329:ba0ae5de62d1 | 330:407684f806e4 |
|---|---|
| 163 regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) | 163 regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) |
| 164 | 164 |
| 165 -- | 165 -- |
| 166 -- if (Derivative r is finite, regex→automaton is finite | 166 -- if (Derivative r is finite, regex→automaton is finite |
| 167 -- | 167 -- |
| 168 drive-is-finite : (r : Regex Σ) → FiniteSet (Derivative r) | 168 -- drive-is-finite : (r : Regex Σ) → FiniteSet (Derivative r) |
| 169 drive-is-finite ε = {!!} | 169 -- drive-is-finite ε = {!!} |
| 170 drive-is-finite φ = {!!} | 170 -- drive-is-finite φ = {!!} |
| 171 drive-is-finite (r *) = {!!} where | 171 -- drive-is-finite (r *) = {!!} where |
| 172 d1 : FiniteSet (Derivative r ) | 172 -- d1 : FiniteSet (Derivative r ) |
| 173 d1 = drive-is-finite r | 173 -- d1 = drive-is-finite r |
| 174 drive-is-finite (r & r₁) = {!!} | 174 -- drive-is-finite (r & r₁) = {!!} |
| 175 drive-is-finite (r || r₁) = {!!} | 175 -- drive-is-finite (r || r₁) = {!!} |
| 176 drive-is-finite < x > = {!!} | 176 -- drive-is-finite < x > = {!!} |
| 177 | 177 -- |