--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 13:05:18 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 13:32:46 2023 +0900
@@ -165,7 +165,7 @@
     sub*   : {x y : Regex Σ} → SB x y  → SB (x *) y
     sub&1  : (x y z : Regex Σ) → SB x z → SB (x & y) z
     sub&2  : (x y z : Regex Σ) → SB y z → SB (x & y) z
---     sub&<  : (x y : Regex Σ) → rank x < rank y  → SB y x → SB y (x & y) 
+    sub&<  : (x y : Regex Σ) → rank x < rank y  → SB y x → SB y (x & y) 
 
 record ISB (r : Regex Σ) : Set where
     field
@@ -174,60 +174,55 @@
 
 open import bijection using ( InjectiveF ; Is )  
 
-regex∨ : {x y : Regex Σ} →  Bijection (One ∨ ISB x ∨ ISB y) (ISB (x || y))
-regex∨ {x} {y} = record {  fun← = ? ; fun→  = ? ; fiso← = ? ;  fiso→ = ? } where
-    fb00 : ISB (x || y) → One ∨ ISB x ∨ ISB y
-    fb00 record { s = .(x || y) ; is-sub = sunit } = case1 one
-    fb00 record { s = s ; is-sub = sub|1 is-sub } = case2 (case1 record { s = s ; is-sub = is-sub } )
-    fb00 record { s = s ; is-sub = sub|2 is-sub } = case2 (case2 record { s = s ; is-sub = is-sub } )
-
-finSB : (r : Regex Σ) → FiniteSet (ISB r)
-finSB ε = record { finite = 1 ; Q←F = λ _ → record { s = ε ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb00 ; finiso← = fin1≡0  } where
-    fb00 : (q : ISB ε) → record { s = ε ; is-sub = sunit } ≡ q
-    fb00 record { s = ε ; is-sub = sunit } = refl
-finSB φ = ?
-finSB (r *) = ?
-finSB (x & y) = iso-fin (fin-∨1 (fin-∨ (finSB x) (finSB y))) ?
-finSB (x || y) = iso-fin (fin-∨1 (fin-∨ (finSB x) (finSB y))) ?
-finSB < x > = record { finite = 1 ; Q←F = λ _ → record { s = < x > ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = fb00 ; finiso← = fin1≡0  } where
-    fb00 : (q : ISB < x > ) → record { s = < x >  ; is-sub = sunit } ≡ q
-    fb00 record { s = < x > ; is-sub = sunit } = refl
+finISB2 : {r z : Regex Σ} → FiniteSet ( ISB z) → FiniteSet (SB r z)
+finISB2 = ?
 
-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 
+finISB : (r : Regex Σ) → FiniteSet (ISB r)
+finISB ε = record { finite = 1 ;  Q←F = λ _ → record { s = ε ; is-sub = sunit } ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = fin1≡0  } where
+    fb00 : (q : ISB ε) → record { s = ε ; is-sub = sunit } ≡ q
+    fb00 record { s = .ε ; is-sub = sunit } = refl
+finISB φ = ?
+finISB < x > = ?
+finISB (x || y) = iso-fin (fin-∨1 (fin-∨ (finISB x) (finISB y))) ? where
+     fb00 : ISB (x || y) → ?
+     fb00 record { s = .(x || y) ; is-sub = sunit } = ?
+     fb00 record { s = s ; is-sub = (sub|1 is-sub) } = ?
+     fb00 record { s = s ; is-sub = (sub|2 is-sub) } = ?
+     fb00 record { s = (z & (x || y)) ; is-sub = (sub&< z (x || y) lt is-sub) } = ? where
+         fb01 : FiniteSet (ISB z)
+         fb01 = finISB z
+finISB (x & y) = ? where
+     fb00 : ISB (x & y) → ?
+     fb00 record { s = .(x & y) ; is-sub = sunit } = ?
+     fb00 record { s = s ; is-sub = (sub&1 .x .y .s is-sub) } = ?
+     fb00 record { s = s ; is-sub = (sub&2 .x .y .s is-sub) } = ?
+     fb00 record { s = (z & (x & y)) ; is-sub = (sub&< z (x & y) lt is-sub) } = ? where
+         fb01 : FiniteSet (ISB z)
+         fb01 = finISB z
+finISB (x *) = ? where
+     fb00 : ISB (x *) → ?
+     fb00 record { s = .(x *) ; is-sub = sunit } = ?
+     fb00 record { s = s ; is-sub = (sub* is-sub) } = ?
+     fb00 record { s = (z & (x *)) ; is-sub = (sub&< z (x *) lt is-sub) } = ? where
+         fb01 : FiniteSet (ISB z)
+         fb01 = finISB z
 
-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   Σ) →  CISB r → Bool
+toSB : (r : Regex   Σ) →  ISB r → Bool
 toSB r cr = ?
 
-sbempty? : (r : Regex Σ) → (CISB r → Bool) → Bool
+sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
 sbempty? r = ?
 
-sbderive : (r : Regex Σ) →  (CISB r → Bool) → Σ → CISB r  → Bool
+sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r  → Bool
 sbderive = ?
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
 
-finSBTA : (r : Regex Σ) → FiniteSet (CISB r → Bool)
-finSBTA r = fin→ ( finCISB r )
+finSBTA : (r : Regex Σ) → FiniteSet (ISB r → Bool)
+finSBTA r = fin→ ( finISB r )
 
-regex→automaton1 : (r : Regex   Σ) → Automaton (CISB r  → Bool) Σ
+regex→automaton1 : (r : Regex   Σ) → Automaton (ISB r  → Bool) Σ
 regex→automaton1 r = record { δ = sbderive r ; aend = sbempty? r }
 
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool