--- a/automaton-in-agda/src/derive.agda	Sat Jul 22 11:10:23 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Jul 22 11:28:14 2023 +0900
@@ -51,7 +51,7 @@
 
 data regex-states (x : Regex  Σ ) : Regex  Σ → Set where
     unit   : regex-states x x
-    derive : { y : Regex  Σ } → regex-states x y → (s : Σ)  → regex-states x ( derivative y s )
+    derive : { y z : Regex  Σ } → regex-states x y → (s : Σ) →  z ≡ derivative y s → ¬ (x ≡ z) → regex-states x z
 
 record Derivative (x : Regex  Σ ) : Set where
     field
@@ -61,10 +61,10 @@
 open Derivative
 
 derive-step : (r : Regex   Σ) (d0 : Derivative r) → (s : Σ) → regex-states r (derivative (state d0) s)
-derive-step r d0 s = derive (is-derived d0) s
+derive-step r d0 s = derive (is-derived d0) s refl ?
 
 regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
-regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s} 
+regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s refl ? } 
    ; aend = λ d → empty? (state d) }  
 
 regex-match : (r : Regex   Σ) →  (List Σ) → Bool
@@ -148,18 +148,19 @@
          fl04 : Is (Derivative ε) (SB ε 0 → Bool) fb02 a → a sbε ≡ true
          fl04 n = sym (cong (λ k → k sbε) (Is.fa=c n))
     fl06 :  (y : Regex Σ) → ¬ ( regex-states ε y )
-    fl06 ε s = ?
-    fl06 φ s = ?
-    fl06 (r *) s = ?
-    fl06 (r & r₁) s = ?
-    fl06 (r || r₁) s = ?
-    fl06 < x > s = ?
+    fl06 ε unit = ?
+    fl06 ε (derive s s₁ x ne) = ?
+    fl06 φ (derive s s₁ x ne) = fl06 _ s
+    fl06 (r *) (derive s s₁ x ne) = fl06 _ s
+    fl06 (r & r₁) (derive s s₁ x ne) = fl06 _ s
+    fl06 (r || r₁) (derive s s₁ x ne) = fl06 _ s
+    fl06 < x > (derive s s₁ x₁ ne) = fl06 _ s
     fl05 :  {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y
     fl05 {x} {y} eq with is-derived x | inspect is-derived x | is-derived y | inspect is-derived y
     ... | unit | record { eq = refl } | unit | record { eq = refl } = refl
-    ... | unit | record { eq = refl } | derive s s₁ | record { eq = refl } = ⊥-elim (fl06 _ s)
-    ... | derive e s | record { eq = eq1 } | unit | t = ?
-    ... | derive e s | record { eq = refl } | derive s1 s₁ | record { eq = refl}  = ?
+    ... | unit | record { eq = refl } | derive s s₁ eqz ne | record { eq = refl } = ⊥-elim (fl06 _ s)
+    ... | derive {y1} {z1} e s eqz0 ne | record { eq = refl } | unit | record { eq = refl} = ?
+    ... | derive e s eqz0 ne0 | record { eq = refl } | derive s1 s₁  eqz1 ne1 | record { eq = refl}  = ?
 SBN φ = ?
 SBN (r *) = ?
 SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? }