--- a/automaton-in-agda/src/derive.agda	Sat Nov 27 11:08:59 2021 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Dec 18 16:27:46 2021 +0900
@@ -17,6 +17,8 @@
 open import regex
 open FiniteSet
 
+-- whether a regex accepts empty input
+--
 empty? : Regex  Σ → Bool
 empty?  ε       = true
 empty?  φ       = false
@@ -160,3 +162,16 @@
    regex-derive0 [] t = t
    regex-derive0 (x ∷ r) t = regex-derive0 r (regex-derive1 x (to-list fin (λ _ → true)) t) 
 
+--
+-- if (Derivative r is finite,  regex→automaton is finite
+--
+drive-is-finite : (r : Regex   Σ) → FiniteSet (Derivative r) 
+drive-is-finite ε = {!!}
+drive-is-finite φ = {!!}
+drive-is-finite (r *) = {!!} where
+   d1 :  FiniteSet (Derivative r )
+   d1 = drive-is-finite r
+drive-is-finite (r & r₁) = {!!}
+drive-is-finite (r || r₁) = {!!}
+drive-is-finite < x > = {!!}
+