--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 11:18:43 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 13:05:18 2023 +0900
@@ -193,59 +193,41 @@
     fb00 : (q : ISB < x > ) → record { s = < x >  ; is-sub = sunit } ≡ q
     fb00 record { s = < x > ; is-sub = sunit } = refl
 
-data ISBn : (r : Regex Σ) →  Set where
-     &unit : (r : Regex Σ) → (i : ISB r ) → ISBn r
-     &next : (r y : Regex Σ) → (x : ISB r) → ISBn y → rank y < rank (ISB.s x) → ISBn (y & ISB.s x )
+data ISBn (r : Regex Σ) : ( rs : Regex Σ ) →   Set where
+     unit : (rs : ISB r ) → ISBn r (ISB.s rs)
+     next : (ys : Regex Σ) → (x : ISB r) → ISBn r ys → rank ys < rank (ISB.s x) → ISBn r (ys & ISB.s x) 
+
+record CISB (r : Regex Σ) : Set where
+     field
+        rg : Regex Σ
+        isbn : ISBn r rg 
 
-finISBn : (r : Regex Σ) → FiniteSet (ISBn r)
-finISBn ε = record { finite = 1 ; Q←F = λ _ → fb01 ; F←Q = λ _ → # 0 ; finiso→ = fb00 ; finiso← = fin1≡0  } where
-      fb01 : ISBn ε
-      fb01 = &unit ε record { s = ε ; is-sub = sunit }
-      fb00 : (q : ISBn ε) → fb01 ≡ q
-      fb00 (&unit .ε record { s = .ε ; is-sub = sunit }) = refl
-finISBn φ = ?
-finISBn < x > = ?
-finISBn (r *) = ?
-finISBn (x || y) = iso-fin (fin-∨1 (fin-∨ (finISBn x) (finISBn y))) record { fun← = fb00 ; fun→ = ? ; fiso← = ? ; fiso→ = ? } where
-   fb00 : ISBn (x || y) → One ∨ ISBn x ∨ ISBn y
-   fb00 (&unit .(x || y) record { s = .(x || y) ; is-sub = sunit }) = case1 one
-   fb00 (&unit .(x || y) record { s = s ; is-sub = (sub|1 is-sub) }) = case2 (case1 (&unit x record { s = s ; is-sub = is-sub } ))
-   fb00 (&unit .(x || y) record { s = s ; is-sub = (sub|2 is-sub) }) = case2 (case2 (&unit y record { s = s ; is-sub = is-sub } ))
-finISBn (x & y) = iso-fin (fin-∨ (fin-∨1 (fin-∨ (finISBn x) (finISBn y))) (fin-∧ (finISBn x) (finISBn y)) ) 
-      record { fun← = fb00 ; fun→ = ? ; fiso← = ? ; fiso→ = ? }  where
-   fb00 :  ISBn (x & y) → (One ∨ ISBn x ∨ ISBn y) ∨ (ISBn x ∧ ISBn y)
-   fb00 (&unit .(x & y) record { s = .(x & y) ; is-sub = sunit }) = case1 (case1 one)
-   fb00 (&unit .(x & y) record { s = s ; is-sub = (sub&1 .x .y .s is-sub) }) 
-       = case1 (case2 (case1 (&unit _ record { s = s ; is-sub = is-sub })))
-   fb00 (&unit .(x & y) record { s = s ; is-sub = (sub&2 .x .y .s is-sub) }) 
-       = case1 (case2 (case2 (&unit _ record { s = s ; is-sub = is-sub })))
-   fb00 (&next r s x d s<x) = case2 ⟪ d , &unit _ record { s = _ ; is-sub = sunit } ⟫
-   fb01 : (One ∨ ISBn x ∨ ISBn y) ∨ (ISBn x ∧ ISBn y) → ISBn (x & y)
-   fb01 (case1 (case1 one)) = &unit (x & y) record { s = (x & y) ; is-sub = sunit } 
-   fb01 (case1 (case2 (case1 (&unit .x record { s = s ; is-sub = is-sub })))) = &unit (x & y) record { s = s ; is-sub = sub&1 x y s is-sub }
-   fb01 (case1 (case2 (case1 (&next r y x sx x₁)))) = ?
-   fb01 (case1 (case2 (case2 sy))) = ?
-   fb01 (case2 x) = ?
+finCISB : (r : Regex Σ) → FiniteSet (CISB r)
+finCISB ε = record { finite = 1 ; Q←F = λ _ → ? ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = fin1≡0  } where
+finCISB φ = ?
+finCISB < x > = ?
+finCISB (r *) = ?
+finCISB (x || y) = iso-fin (fin-∨1 (fin-∨ (finCISB x) (finCISB y))) record { fun← = ? ; fun→ = ? ; fiso← = ? ; fiso→ = ? } where
+     fb00 :  CISB (x || y) → One ∨ CISB x ∨ CISB y
+     fb00 record { rg = rg ; isbn = isbn } = ?
+finCISB (r & r₁) = ?
 
-toSB : (r : Regex   Σ) →  ISBn r → Bool
-toSB .(y & ISB.s x) (&next r y x is x₁) = false
-toSB r (&unit .r i) with rg-eq? r (ISB.s i)
-... | yes _ = true
-... | no _ = false
+toSB : (r : Regex   Σ) →  CISB r → Bool
+toSB r cr = ?
 
-sbempty? : (r : Regex Σ) → (ISBn r → Bool) → Bool
+sbempty? : (r : Regex Σ) → (CISB r → Bool) → Bool
 sbempty? r = ?
 
-sbderive : (r : Regex Σ) →  (ISBn r → Bool) → Σ → ISBn r  → Bool
+sbderive : (r : Regex Σ) →  (CISB r → Bool) → Σ → CISB r  → Bool
 sbderive = ?
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
 
-finSBTA : (r : Regex Σ) → FiniteSet (ISBn r → Bool)
-finSBTA r = fin→ ( finISBn r )
+finSBTA : (r : Regex Σ) → FiniteSet (CISB r → Bool)
+finSBTA r = fin→ ( finCISB r )
 
-regex→automaton1 : (r : Regex   Σ) → Automaton (ISBn r  → Bool) Σ
+regex→automaton1 : (r : Regex   Σ) → Automaton (CISB r  → Bool) Σ
 regex→automaton1 r = record { δ = sbderive r ; aend = sbempty? r }
 
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool