--- a/automaton-in-agda/src/derive.agda	Mon Jul 10 12:59:01 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 10 14:07:36 2023 +0900
@@ -94,8 +94,10 @@
 rank < x > = 0
 
 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ε : (r : Regex Σ) → SB ε 0
+    sbφ : (r : Regex Σ) → SB φ 0
+    sb<> : (s : Σ) → SB < s > 0
+    sb| : (x y : Regex Σ) → (xn yn xy : ℕ) → SB x xn → SB y yn → xy ≡  max xn yn  → SB (x || y)  xy
     sb* : (x : Regex Σ) → (xn : ℕ) → SB (x & (x *)) (suc xn)
     sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → SB (x & y) (suc yn)
 
@@ -118,10 +120,13 @@
 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 = ?
+     fb01 zero .ε eq d (sbε r) = true
+     fb01 zero .φ eq d (sbφ r) = false
+     fb01 zero .(< s >) eq d (sb<> s) = ?
+     fb01 zero .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) = ?
+     fb01 (suc n) .(x || y) eq d (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) = ?
+     fb01 (suc n) .(x & (x *)) eq d (sb* x .(max (rank x) (rank (x *)))) = ?
+     fb01 (suc n) .(x & y) eq d (sb& x y xn .(max (rank x) (rank y)) x₁) = ?
 
 finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
 finite-derivative r = inject-fin (finSBTA r) (injSB r) ?