--- a/automaton-in-agda/src/derive.agda	Sat Jul 22 14:50:31 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Jul 22 15:37:44 2023 +0900
@@ -155,44 +155,35 @@
 dec-regex < x > s = ?
 
 
-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 )
+toSB : (r : Regex   Σ) →  SB r (rank r) → Bool
+toSB ε sbε = true
+toSB φ sbφ = true
+toSB (r *) (sb* .r .(rank r) x) = toSB r x
+toSB (r & r₁) (sb& .r .r₁ xn .(max (rank r) (rank r₁)) x<m x₁ x₂) = toSB r ?  /\ toSB r₁ ?
+toSB (r || r₁) x = toSB r ?  \/ toSB r₁ ?
+toSB < x₁ > (sb<> .x₁) = true
 
-SBN : (r : Regex   Σ) → SBf r (rank r)
-SBN ε = record { rank=n = refl ; f = fb02 ; sb-inject = fl05 ; dec = fl03 } where
-    fb02 : Derivative ε → SB ε 0 → Bool
-    fb02 d sbε with dec-regex ε (state d)
-    ... | yes _ = true
-    ... | no _  = false
-    fl03 : (a : SB ε 0 → Bool) → Dec (Is (Derivative ε) (SB ε 0 → Bool) fb02 a)
-    fl03 a with a sbε | inspect a sbε
-    ... | true | record { eq = eq1 } = yes ? 
-    ... | false | record { eq = eq1} = no ? 
-    fl05 :  {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y
-    fl05 {x} {y} eq with dec-regex ε (state x)  | dec-regex ε (state y) | cong (λ k → k sbε) eq
-    ... | yes eqx | yes eqy | _ = ?
-    ... | yes eqx | no neqy | ()
-    ... | no neqx | yes eqy | ()
-    ... | no neqx | no neqy | _ with is-derived x | inspect is-derived x | is-derived y | inspect is-derived y
-    ... | unit refl | record { eq = refl } | unit refl | record { eq = refl } = refl
-    ... | unit refl | record { eq = refl } | derive s s₁ zeq | record { eq = refl } = ⊥-elim ( neqx refl )
-    ... | derive {y1}  e s zeq | record { eq = refl } | unit refl | record { eq = refl} = ⊥-elim ( neqy refl )
-    ... | derive {x1} e s refl | record { eq = refl } | derive {y1} s1 s₁ refl | record { eq = refl}  = ? 
-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 = ? } 
+sbempty? : (r : Regex Σ) → SB r (rank r) → Bool
+sbempty? .ε sbε = true
+sbempty? .φ sbφ = false
+sbempty? .(< s >) (sb<> s) = false
+sbempty? .(x || y) (sb| x y xn yn .(rank (x || y)) sb sb₁ x₁) = sbempty? ? ? \/ sbempty? ? ?
+sbempty? .(x *) (sb* x .(rank x) sb) = true
+sbempty? .(x & y) (sb& x y xn .(max (rank x) (rank y)) x₁ sb sb₁) = sbempty? ? ? /\ sbempty? ? ?
+
+sbderive : (r : Regex Σ) →  (SB r (rank r) → Bool) → Σ → SB r (rank r) → Bool
+sbderive ε f s sbε = f sbε
+sbderive φ f s sbφ = false
+sbderive (r *) f s (sb* .r .(rank r) sb) = ?
+sbderive (r & r₁) f s sb = ?
+sbderive (r || r₁) f s sb = ?
+sbderive < x > f s sb = ?
 
 regex→automaton1 : (r : Regex   Σ) → Automaton (SB r (rank r) → Bool) Σ
-regex→automaton1 r = record { δ = λ d s → ? ; aend = λ d → ? }  
+regex→automaton1 r = record { δ = sbderive r ; aend = λ d → ? }  
 
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool
-regex-match1 r is = accept ( regex→automaton1 r ) ? is
+regex-match1 r is = accept ( regex→automaton1 r ) (λ sb → toSB r sb) is