--- a/automaton-in-agda/src/derive.agda	Thu Aug 10 09:59:47 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Sep 24 11:32:01 2023 +0900
@@ -238,6 +238,9 @@
      fb00 record { s = s ; is-sub = (sub* is-sub) } = {!!}
      fb00 record { s = (z & (x *)) ; is-sub = (sub*& z x lt is-sub) } = case1 record { z = z ; is-sub = is-sub ; lt = lt }
 
+d-ISB : (r : Regex Σ) → ISB r → (s : Σ) → ISB r → Bool
+d-ISB r x s y = ?
+
 toSB : (r : Regex   Σ) →  ISB r → Bool
 toSB r record { s = s ; is-sub = is-sub } with rg-eq? r s
 ... | yes _ = true
@@ -274,24 +277,8 @@
 sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r → Bool
 sbderive ε f s record { s = .ε ; is-sub = sε } = false
 sbderive φ f s record { s = t ; is-sub = sφ } = false
-sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } with f record { s = t ; is-sub = sub* is-sub } 
-... | false = true
-... | true with derivative r s
-... | ε = true
-... | φ = false
-... | t₁ * = false
-... | t₁ & t₂ = false
-... | t₁ || t₂ = false
-... | < x > = false
-sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } with f record { s = (x & (r *)) ; is-sub = sub*& x r x₁ is-sub } 
-... | false = true
-... | true with derivative r s
-... | ε = false
-... | φ = false
-... | t₁ * = true
-... | t₁ & t₂ = true
-... | t₁ || t₂ = true
-... | < s > = true
+sbderive (r *) f s record { s = t ; is-sub = sub* is-sub } = ?
+sbderive (r *) f s record { s = .(x & (r *)) ; is-sub = sub*& x .r x₁ is-sub } = ?
 sbderive (r & r₁) f s record { s = t ; is-sub = sub&1 .r .r₁ .t is-sub } with f record { s = t ; is-sub = sub&1 r r₁ t is-sub } 
 ... | false = true
 ... | true = false