--- a/automaton-in-agda/src/derive.agda	Sun Aug 06 09:48:27 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Thu Aug 10 09:29:03 2023 +0900
@@ -12,6 +12,7 @@
 open import automaton
 open import logic
 open import regex
+open import regular-language
 
 -- whether a regex accepts empty input
 --
@@ -332,40 +333,40 @@
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool
 regex-match1 r is = accept ( regex→automaton1 r ) (λ sb → toSB r sb) is
 
+rg00 : (x : Σ) (y : List Σ) → {r : Regex Σ} → (d : Derivative r) → state d ≡ φ  → accept (regex→automaton r) 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-ε : (r : Regex Σ) → (s : Σ) → r ≡ ε → derivative r s ≡ φ
+derive-ε r s refl = refl
+
 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₁) = 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 ε (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) 
 derive-is-regex-language φ [] = refl
-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 φ (x ∷ x₁) = sym (rg00 x x₁ record { state = φ ; is-derived = derive (unit refl) _ refl} refl) 
+derive-is-regex-language (r *) []  with empty? (r *)
+... | true = refl
+... | false = refl
+derive-is-regex-language (r *) (h ∷ x) = ?  where
+    rg03 : (x s : Σ) → ?
+    rg03 = ?
 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₁) [] = cong₂ (λ j k → j \/ k ) (derive-is-regex-language r []) (derive-is-regex-language r₁ []) 
 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₃) = sym rg02 where
-    rg01 : Dec ( x₁ ≡ x ) →  regex-language < x₁ > eq? (x ∷ x₂ ∷ x₃ ) ≡ false
-    rg01 (yes eq) = refl
-    rg01 (no neq) = refl
+derive-is-regex-language < x₁ > (x ∷ x₂ ∷ x₃) = sym rg02  where
     rg03 : (x s : Σ) → (derivative < x > s ≡ ε ) ∨ (derivative < x > s ≡ φ )
     rg03 x s with eq? x s
     ... | yes _ = case1 refl
     ... | no _ = case2 refl
     rg02 : regex-match < x₁ > (x ∷ x₂ ∷ x₃ ) ≡ false
     rg02 with rg03 x₁ x
-    ... | case1 eq = ?
-    ... | case2 eq = ?
+    ... | case2 eq = rg00 x (x₂ ∷ x₃) record { state = _ ; is-derived = derive (unit refl) _ refl} eq
+    ... | case1 eq = rg00 x₂ x₃ record { state = _ ; is-derived = derive (derive (unit refl) _ refl) _ refl } (derive-ε  _ _ eq )
 --    immediate with eq? x₁ x generates an error w != eq? a b of type Dec (a ≡ b)
 
 derive=ISB : (r : Regex Σ) → (x : List Σ )→ regex-match r x ≡ regex-match1 r x

--- a/automaton-in-agda/src/regular-language.agda	Sun Aug 06 09:48:27 2023 +0900
+++ b/automaton-in-agda/src/regular-language.agda	Thu Aug 10 09:29:03 2023 +0900
@@ -36,14 +36,17 @@
 Star1 {Σ} A [] = true
 Star1 {Σ} A (h ∷ t) = split A ( Star1 {Σ} A ) (h ∷ t)
 
+-- Terminating version of Star1
+--
 repeat : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
+repeat2 : {Σ : Set} → (x : List Σ → Bool) → (pre y : List Σ ) → Bool
+repeat2 x pre [] = false
+repeat2 x pre (h ∷ y) = 
+   (x (pre ++ (h ∷ [])) /\ repeat x y )
+   \/ repeat2 x (pre ++ (h ∷ [])) y 
+
 repeat {Σ} x [] = true
-repeat {Σ} x (h ∷ y) = repeat2 [] (h ∷ y) where
-    repeat2 : (pre y : List Σ ) → Bool
-    repeat2 pre [] = false
-    repeat2 pre (h ∷ y) = 
-       (x (pre ++ (h ∷ [])) /\ repeat x y )
-       \/ repeat2 (pre ++ (h ∷ [])) y 
+repeat {Σ} x (h ∷ y) = repeat2 x [] (h ∷ y) 
 
 Star : {Σ : Set} → (x : List Σ → Bool) → (y : List Σ ) → Bool 
 Star {Σ} x y = repeat x y