--- a/automaton-in-agda/src/derive.agda	Mon Jul 10 14:07:36 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 10 14:28:39 2023 +0900
@@ -120,13 +120,15 @@
 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 .ε 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₁) = ?
+     fb01 n r eq d sb with is-derived d 
+     fb01 n r eq d sb | unit = true
+     fb01 zero .ε eq d (sbε r) | derive {y} ss i = true
+     fb01 zero .φ eq d (sbφ r) | derive {y} ss i = false
+     fb01 zero .(< s >) eq d (sb<> s) | derive {y} ss i = ?
+     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 & (x *)) eq d (sb* x .(max (rank x) (rank (x *)))) | derive {y₂} ss i = ?
+     fb01 (suc n) .(x & y) eq d (sb& x y xn .(max (rank x) (rank y)) x₁) | derive {y₂} ss i = ?
 
 finite-derivative : (r : Regex   Σ) → FiniteSet (Derivative r) 
 finite-derivative r = inject-fin (finSBTA r) (injSB r) ?