--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 04:14:52 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 10:10:44 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 x y → 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,28 +174,60 @@
 
 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 = ?
+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) = ?
+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
 
+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 )
 
-toSB : (r : Regex   Σ) →  ISB r → Bool
-toSB r isb with rg-eq? r (ISB.s isb)
+finISBn : (r : Regex Σ) → FiniteSet (ISBn r)
+finISBn r = ? where
+    f : InjectiveF (ISBn r) (ISBn r)
+    f = ?
+    fb01 : (i : ℕ ) → rank r ≤ i → FiniteSet (ISBn r)
+    fb01 zero le = iso-fin (finSB r) ? 
+    fb01 (suc i) le = iso-fin (fin-∨ (finSB r) (fin-∧ (finSB r) (inject-fin ? ? ?) ))  
+        record {  fun← = ? ; fun→  = ? ; fiso← = ? ;  fiso→ = ? }  where
+        f1 : ISBn r → ISB r ∨ (ISB r ∧ ? )
+        f1 (&unit .r i) = case1 i
+        f1 (&next r y x x₁ x₂) = case2 ?
+
+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
 
-sbempty? : (r : Regex Σ) → (ISB r → Bool) → Bool
+sbempty? : (r : Regex Σ) → (ISBn r → Bool) → Bool
 sbempty? r = ?
 
-sbderive : (r : Regex Σ) →  (ISB r → Bool) → Σ → ISB r  → Bool
+sbderive : (r : Regex Σ) →  (ISBn r → Bool) → Σ → ISBn r  → Bool
 sbderive = ?
 
 -- finDerive : (r : Regex Σ) → FiniteSet (Derived r)
 --    this is not correct because it contains s || s || s || .....
 
-finSBTA : (r : Regex Σ) → FiniteSet (ISB r → Bool)
-finSBTA r = fin→ ( finSB r )
+finSBTA : (r : Regex Σ) → FiniteSet (ISBn r → Bool)
+finSBTA r = fin→ ( finISBn r )
 
-regex→automaton1 : (r : Regex   Σ) → Automaton (ISB r  → Bool) Σ
+regex→automaton1 : (r : Regex   Σ) → Automaton (ISBn r  → Bool) Σ
 regex→automaton1 r = record { δ = sbderive r ; aend = sbempty? r }
 
 regex-match1 : (r : Regex   Σ) →  (List Σ) → Bool