--- a/automaton-in-agda/src/derive.agda	Sat Jul 22 10:04:39 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Jul 22 12:58:38 2023 +0900
@@ -70,14 +70,7 @@
 regex-match : (r : Regex   Σ) →  (List Σ) → Bool
 regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
 
-open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
-
-D-cong :  (r s : Regex Σ) → (x : Derivative r) (y : Derivative s) 
-   → state x ≡ state y → is-derived x ≅ is-derived y  → x ≅ y
-D-cong = ?
-
-D-inject :  (r : Regex Σ) → {x y : Derivative r} → x ≡ y
-D-inject r {x} {y} = HE.≅-to-≡  (D-cong r r x y ? ? )
+-- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
 -- open import nfa
 open import Data.Nat
@@ -134,6 +127,34 @@
     fb00 (suc n) φ z≤n =  fb00 n φ z≤n 
     fb00 (suc n) < x > z≤n = fb00 n < x > z≤n 
 
+dec-regex : (r s : Regex Σ) → Dec ( r ≡ s )
+dec-regex ε ε = yes refl
+dec-regex ε φ = no (λ ())
+dec-regex ε (s *) = no (λ ())
+dec-regex ε (s & s₁) = no (λ ())
+dec-regex ε (s || s₁) = no (λ ())
+dec-regex ε < x > = no (λ ())
+dec-regex φ ε = no (λ ())
+dec-regex φ φ = yes refl
+dec-regex φ (s *) = no (λ ())
+dec-regex φ (s & s₁) = no (λ ())
+dec-regex φ (s || s₁) = no (λ ())
+dec-regex φ < x > = no (λ ())
+dec-regex (r *) ε = no (λ ())
+dec-regex (r *) φ = no (λ ())
+dec-regex (r *) (s *) with dec-regex r s
+... | yes eq = yes ( cong (_*) eq)
+... | no ne = no (λ eq → ne (fb10 eq) ) where
+     fb10 : {r s : Regex Σ} → (r *) ≡ (s *) → r ≡ s 
+     fb10  refl = refl
+dec-regex (r *) (s & s₁) = no (λ ())
+dec-regex (r *) (s || s₁) = no (λ ())
+dec-regex (r *) < x > = no (λ ())
+dec-regex (r & r₁) s = ?
+dec-regex (r || r₁) s = ?
+dec-regex < x > s = ?
+
+
 record SBf (r : Regex Σ) (n : ℕ) : Set where
     field
        rank=n    : rank r ≡ n
@@ -144,23 +165,24 @@
 SBN : (r : Regex   Σ) → SBf r (rank r)
 SBN ε = record { rank=n = refl ; f = fb02 ; sb-inject = fl05 ; dec = fl03 } where
     fb02 : Derivative ε → SB ε 0 → Bool
-    fb02 d sbε = true
+    fb02 d sbε with dec-regex ε (state d)
+    ... | yes _ = true
+    ... | no _  = false
     fl03 : (a : SB ε 0 → Bool) → Dec (Is (Derivative ε) (SB ε 0 → Bool) fb02 a)
     fl03 a with a sbε | inspect a sbε
-    ... | true | record { eq = eq1 } = yes record { a = record { state = ε ; is-derived = unit } 
-         ; fa=c = f-extensionality fl04 } where
-         fl04 : (x : SB ε 0) →  fb02 (record { state = ε ; is-derived = unit }) x ≡ a x
-         fl04 sbε = sym eq1
-    ... | false | record { eq = eq1} = no (λ n → ¬-bool {a sbε} eq1 (fl04 n)) where
-         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 Σ) → (s : Σ) → ¬ ( regex-states y ε )
-    fl06 y s x with derivative y s | inspect (derivative y) s
-    ... | d | record { eq = eq1 } = ?
+    ... | 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 is-derived x | inspect is-derived x 
-    ... | unit | record { eq = eq1 } = ?
-    ... | derive e s | record { eq = eq1 } = ?
+    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 | _ = ?
+
 SBN φ = ?
 SBN (r *) = ?
 SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? }