--- a/automaton-in-agda/src/derive.agda	Mon Jul 10 11:52:28 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 10 12:59:01 2023 +0900
@@ -95,23 +95,37 @@
 
 data SB : (r : Regex Σ) → (rn : ℕ) → Set where
     sb0 : (r : Regex Σ) → (rn : ℕ) → SB r rn
+    -- sb| : (x y r : Regex Σ) → (xn yn xy : ℕ) → SB x xn → SB y yn → xy ≡  max xn yn  → (x || y) ≡ r  → SB r xy 
     sb* : (x : Regex Σ) → (xn : ℕ) → SB (x & (x *)) (suc xn)
     sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → SB (x & y) (suc yn)
 
-record SBS (r : Regex Σ) : Set where
-   field
-      s : Regex Σ
-      rn : ℕ 
-      sb : SB r rn
-
-SBTA : (r : Regex Σ) → Automaton (SBS r → Bool) Σ
+SBTA : (r : Regex Σ) → Automaton (SB r (rank r) → Bool) Σ
 SBTA = ?
 
-finSBTA : (r : Regex Σ) → FiniteSet (SBS r → Bool)
-finSBTA = ?
+open import bijection using ( InjectiveF ; Is )  
 
-finie-deverive : (r : Regex Σ) → (c : Σ) → (x : List Σ) → regex-match r x ≡ true → accept (SBTA r) ? x ≡ true
-finie-deverive = ?
+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 = ?
+
+injSB : (r : Regex   Σ) → InjectiveF (Derivative r) (SB r (rank r) → Bool)
+injSB r = record { f = fb01 (rank r) r refl ; inject = ? } where
+     fb01 : (n : ℕ ) →  (r : Regex Σ) →  rank r ≡ n →  Derivative r → SB r (rank r) → Bool
+     fb01 zero r eq record { state = r ; is-derived = unit } sb = ?
+     fb01 zero r eq record { state = t ; is-derived = derive d s } sb = ?
+     fb01 (suc n) r eq record { state = r ; is-derived = unit } sb = ?
+     fb01 (suc n) r eq record { state = t ; is-derived = derive d s } sb = ?
+
+finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
+finite-derivative r = inject-fin (finSBTA r) (injSB r) ?
 
 
 
+

--- a/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 10 11:52:28 2023 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Jul 10 12:59:01 2023 +0900
@@ -638,23 +638,3 @@
         } where
           bp : FiniteSet (B<n n)
           bp = inf00 n (NP.≤-trans a≤sa le )
-   
--- record {
--- finite = ? 
--- ; Q←F = ?
--- ; F←Q =  ?
--- ; finiso→ = ?
--- ; finiso← = ?
--- } where
---    f = InjectiveF.f fi
---    f⁻¹ : (a : A ) → Is B A f a → B
---    f⁻¹ a isa = Is.a isa
--- 
---    record CountB (b : B) : Set where
---       cb : ℕ
---       a : A
---       fb=a : InjectiveF.f fi b ≡ a
--- 
-
-
-