--- a/automaton-in-agda/src/derive.agda	Sun Jul 09 15:37:18 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sun Jul 09 16:03:43 2023 +0900
@@ -72,43 +72,43 @@
 open import Data.Nat
 -- open import Data.Nat hiding ( _<_ ; _>_ )
 -- open import Data.Fin hiding ( _<_ )
+open import nat
 open import finiteSetUtil
 open FiniteSet
 open import Data.Fin hiding (_<_)
 
--- derivative generates   (x & y) || ... form. y and x part is a substerm of original regex
--- since subterm is finite, only finite number of state is generated for each operator 
--- this does not work, becuase it depends on input sequences
--- finite-derivative : (r : Regex  Σ) → FiniteSet Σ  → FiniteSet (Derivative r) 
--- order : Regex  Σ → ℕ
--- decline-derive : (x : Regex Σ ) (i : Σ ) → 0 < order x → order (derivative x i) < order x 
---    is not so easy
--- in case of automaton, number of derivative is limited by iteration of input length, so it is finite.
--- so we cannot say derived automaton is finite i.e. regex-match is regular language now
+-- finiteness of derivative 
+--    term generate   x & y   for each * and & only once
+--      rank : Regex → ℕ 
+--   r₀ & r₁ ... r
 
 open import Relation.Binary.Definitions
 
-data SB : (r s : Regex Σ) → Set where
-    sbε : SB ε ε
-    sbφ : SB φ φ
-    sb*x : (x : Regex Σ) → SB (x *) x
-    sb*  : (x : Regex Σ) → SB (x *) (x *)
-    sb&x : (x y : Regex Σ) → SB (x & y) x
-    sb&y : (x y : Regex Σ) → SB (x & y) y
-    sb& : (x y : Regex Σ) → SB (x & y) (x & y)
-    sb|x : (x y : Regex Σ) → SB (x || y) x
-    sb|y : (x y : Regex Σ) → SB (x || y) y
-    sb| : (x y : Regex Σ) → SB (x || y) (x || y)
-    sb<> : (x : Σ) → SB < x > < x >
+rank : (r : Regex Σ) → ℕ
+rank ε = 0
+rank φ = 0
+rank (r *) = suc (rank r)
+rank (r & r₁) = suc (max (rank r) (rank r₁))
+rank (r || r₁) = max (rank r) (rank r₁)
+rank < x > = 0
+
+data SB : (r : Regex Σ) → (rn : ℕ) → Set where
+    sb0 : (r : Regex Σ) → (rn : ℕ) → SB r rn
+    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 Σ
-      sb : SB r s
+      rn : ℕ 
+      sb : SB r rn
 
-SBTA : (r : Regex Σ) → Automaton (SBS r) Σ
+SBTA : (r : Regex Σ) → Automaton (SBS r → Bool) Σ
 SBTA = ?
 
+finSBTA : (r : Regex Σ) → FiniteSet (SBS r → Bool)
+finSBTA = ?
+
 finie-deverive : (r : Regex Σ) → (c : Σ) → (x : List Σ) → regex-match r x ≡ true → accept (SBTA r) ? x ≡ true
 finie-deverive = ?