--- a/automaton-in-agda/src/derive.agda	Sat Jul 22 12:58:38 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Jul 22 14:50:31 2023 +0900
@@ -50,8 +50,8 @@
 ... | no  _ = φ
 
 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 )
+    unit   : { z : Regex Σ} → z ≡ x → regex-states x z
+    derive : { y z : Regex  Σ } → regex-states x y → (s : Σ) → z ≡  derivative y s → regex-states x z 
 
 record Derivative (x : Regex  Σ ) : Set where
     field
@@ -61,14 +61,14 @@
 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
-regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
+regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit refl } is 
 
 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
@@ -172,26 +172,29 @@
     fl03 a with a sbε | inspect a sbε
     ... | true | record { eq = eq1 } = yes ? 
     ... | false | record { eq = eq1} = no ? 
-    fl07 :  (y : Regex Σ) → regex-states ε y → y ≡ ε
-    fl07 .ε unit = refl
-    fl07 r (derive {y} d s) with fl07 y d
-    ... | t = ?
     fl05 :  {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y
     fl05 {x} {y} eq with dec-regex ε (state x)  | dec-regex ε (state y) | cong (λ k → k sbε) eq
     ... | yes eqx | yes eqy | _ = ?
     ... | yes eqx | no neqy | ()
     ... | no neqx | yes eqy | ()
-    ... | no neqx | no neqy | _ = ?
-
+    ... | no neqx | no neqy | _ with is-derived x | inspect is-derived x | is-derived y | inspect is-derived y
+    ... | unit refl | record { eq = refl } | unit refl | record { eq = refl } = refl
+    ... | unit refl | record { eq = refl } | derive s s₁ zeq | record { eq = refl } = ⊥-elim ( neqx refl )
+    ... | derive {y1}  e s zeq | record { eq = refl } | unit refl | record { eq = refl} = ⊥-elim ( neqy refl )
+    ... | derive {x1} e s refl | record { eq = refl } | derive {y1} s1 s₁ refl | record { eq = refl}  = ? 
 SBN φ = ?
 SBN (r *) = ?
 SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? }
 SBN (r || r₁) = ?
 SBN < x > = record { rank=n = refl ; f = ? ; sb-inject = ? ; dec = ? } 
 
-finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
-finite-derivative r = inject-fin (finSBTA r) record { f = SBf.f (SBN r) ; inject = SBf.sb-inject (SBN r) }  (SBf.dec (SBN r))
+regex→automaton1 : (r : Regex   Σ) → Automaton (SB r (rank r) → Bool) Σ
+regex→automaton1 r = record { δ = λ d s → ? ; aend = λ d → ? }  
+
+regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool
+regex-match1 r is = accept ( regex→automaton1 r ) ? is
 
 
 
 
+