--- a/automaton-in-agda/src/derive.agda	Wed Jul 19 07:58:18 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Wed Jul 19 11:32:23 2023 +0900
@@ -121,13 +121,13 @@
 finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool)
 finSBTA r = fin→ ( fb00 (rank r) r refl ) where
     fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → FiniteSet (SB r (rank r))
-    fb00 zero ε eq = ?
-    fb00 zero φ eq = ?
-    fb00 zero (r || r₁) eq = ?
-    fb00 zero < x > eq = ?
-    fb00 (suc n) (r *) eq = ?
-    fb00 (suc n) (r & r₁) eq = ?
-    fb00 (suc n) (r || r₁) eq = ?
+    fb00 zero ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? }
+    fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? }
+    fb00 zero (r || r₁) eq = iso-fin (fin-∨ (fb00 zero r ?) (fb00 zero r₁ ?)) ?
+    fb00 zero < x > eq = iso-fin fin ?
+    fb00 (suc n) (r *) eq = iso-fin (fb00 n r ?) ?
+    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 
@@ -152,8 +152,23 @@
 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
+       f         : Derivative r → SB r n → Bool
+       sb-inject : {x y : Derivative r} → f x ≡ f y → x ≡ y
+       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 φ = ?
+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) (injSB r) (decdb r)
+finite-derivative r = inject-fin (finSBTA r) record { f = SBf.f (SBN r) ; inject = SBf.sb-inject (SBN r) }  (SBf.dec (SBN r))