--- 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 11:10:23 2023 +0900
@@ -72,13 +72,6 @@
 
 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 nfa
 open import Data.Nat
 open import Data.Nat.Properties
@@ -154,13 +147,19 @@
     ... | 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 } = ?
+    fl06 :  (y : Regex Σ) → ¬ ( regex-states ε y )
+    fl06 ε s = ?
+    fl06 φ s = ?
+    fl06 (r *) s = ?
+    fl06 (r & r₁) s = ?
+    fl06 (r || r₁) s = ?
+    fl06 < x > s = ?
     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 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}  = ?
 SBN φ = ?
 SBN (r *) = ?
 SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? }