--- a/automaton-in-agda/src/derive.agda	Sun Aug 06 00:14:13 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Aug 06 09:48:27 2023 +0900
@@ -317,8 +317,8 @@
     sb00 : ISB r₁ → Bool 
     sb00 record { s = s ; is-sub = is-sub } = f record { s = s ; is-sub = sub|2 is-sub } 
 sbderive < x > f s record { s = .(< x >) ; is-sub = s<> } with eq? x s
-... | yes _  = false
-... | no _  = false
+... | yes _  = false    -- because there is no next state
+... | no _  = true      -- because this term set is empty
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
@@ -334,17 +334,27 @@
 
 derive-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match r x
 derive-is-regex-language ε [] = refl
-derive-is-regex-language ε (x ∷ x₁) = ?
+derive-is-regex-language ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) where
+    rg00 : (x : Σ) (y : List Σ) → (d : Derivative ε) → state d ≡ φ  → accept (regex→automaton ε) d y ≡ false
+    rg00 x [] d refl = refl
+    rg00 x (z ∷ y) record { state = φ ; is-derived = isd } refl = rg00 z y record { state = φ ; is-derived = derive isd z refl } refl 
 derive-is-regex-language φ [] = refl
-derive-is-regex-language φ (x ∷ x₁) = ?
-derive-is-regex-language (r *) x = ?
+derive-is-regex-language φ (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) where
+    rg00 : (x : Σ) (y : List Σ) → (d : Derivative φ) → state d ≡ φ  → accept (regex→automaton φ) d y ≡ false
+    rg00 x [] d refl = refl
+    rg00 x (z ∷ y) record { state = φ ; is-derived = isd } refl = rg00 z y record { state = φ ; is-derived = derive isd z refl } refl 
+derive-is-regex-language (r *) [] = ?
+derive-is-regex-language (r *) (h ∷ x) = ?
 derive-is-regex-language (r & r₁) x = ?
-derive-is-regex-language (r || r₁) x = ?
+derive-is-regex-language (r || r₁) [] = rg04 where
+    rg04 : regex-language r eq? [] \/ regex-language r₁ eq? [] ≡ empty? r \/ empty? r₁
+    rg04 = ?
+derive-is-regex-language (r || r₁) (x ∷ x₁) = ?
 derive-is-regex-language < x₁ > [] = refl
 derive-is-regex-language < x₁ > (x ∷ []) with eq? x₁ x
 ... | yes _  = refl
 ... | no _  = refl
-derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = ? where -- rg01 (eq? x₁ x) where
+derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = sym rg02 where
     rg01 : Dec ( x₁ ≡ x ) →  regex-language < x₁ > eq? (x ∷ x₂ ∷ x₃ ) ≡ false
     rg01 (yes eq) = refl
     rg01 (no neq) = refl
@@ -368,8 +378,8 @@
 derive=ISB (r || r₁) x = ?
 derive=ISB < x₁ > [] = ?
 derive=ISB < x₁ > (x ∷ []) with eq? x₁ x
-... | yes _ = ?
-... | no _ = ?
+... | yes _ = refl
+... | no _ = refl
 derive=ISB < x₁ > (x ∷ x₂ ∷ x₃) = ?
 
 ISB-is-regex-language : (r : Regex Σ) → (x : List Σ )→ regex-language r eq? x ≡  regex-match1 r x