--- a/automaton-in-agda/src/derive.agda	Wed Jul 19 11:32:23 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Fri Jul 21 12:01:16 2023 +0900
@@ -113,9 +113,6 @@
 sb-id (y *) (sb* x t u) | suc k | record{ eq = eq1 } = sb-id y ?
 sb-id (x0 & y0) (sb& .x0 .y0 xn .k x z z₁) | suc k | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ?
 
-SBTA : (r : Regex Σ) → Automaton (SB r (rank r) → Bool) Σ
-SBTA = ?
-
 open import bijection using ( InjectiveF ; Is )  
 
 finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool)
@@ -129,29 +126,6 @@
     fb00 (suc n) (r & r₁) eq = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ?
     fb00 (suc n) (r || r₁) eq = iso-fin (fin-∧ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ?
 
-fb01 : (n : ℕ ) →  (r : Regex Σ) →  rank r ≡ n →  Derivative r → SB r (rank r) → Bool
-fb01 n r eq d sb with is-derived d 
-fb01 n r eq d sb | unit = sb-id r sb
-fb01 zero .ε eq d sbε  | derive {y} ss i = true
-fb01 zero .φ eq d sbφ | derive {y} ss i = true
-fb01 zero .(< s >) eq d (sb<> s) | derive {y} ss i with eq? s i
-... | yes _ = true
-... | no _  = false
-fb01 zero .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
-fb01 (suc n) .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) | derive {y₂} ss i = ?
-fb01 (suc n) .(x *) eq d (sb* x xn u ) | derive {y₂} ss i = ?
-fb01 (suc n) t eq d z | derive {y₂} ss i = ?
-
-injSB : (r : Regex   Σ) → InjectiveF (Derivative r) (SB r (rank r) → Bool)
-injSB r = record { f = fb01 (rank r) r refl ; inject = ? } where
-     fb02 : (x y : Derivative r) → fb01 (rank r) r refl x ≡ fb01 (rank r) r refl y → x ≡ y
-     fb02 = ?
-
-decdb : (r : Regex   Σ) →  (a : SB r (rank r) → Bool) 
-    → Dec (Is (Derivative r) (SB r (rank r) → Bool) (InjectiveF.f (injSB r)) a )
-decdb r a with fb01 (rank r) r refl record { state = r ; is-derived = ? }
-... | t = ?
-
 record SBf (r : Regex Σ) (n : ℕ) : Set where
     field
        rank=n    : rank r ≡ n
@@ -160,12 +134,25 @@
        dec       : (a : SB r n → Bool ) →  Dec (Is (Derivative r) (SB r n → Bool) f a )
 
 SBN : (r : Regex   Σ) → SBf r (rank r)
-SBN ε = record { rank=n = refl ; f = ? ; sb-inject = ? ; dec = ? }
+SBN ε = record { rank=n = refl ; f = fb02 ; sb-inject = fl05 ; dec = fl03 } where
+    fb02 : Derivative ε → SB ε 0 → Bool
+    fb02 d sbε = true
+    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))
+    fl05 :  {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y
+    fl05 {x} {y} eq = ?
 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 = ? }
+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))