# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1690165123 -32400
# Node ID 3f05571385dfef1e876e84e23e59573f5ca78df4
# Parent  b3af758432352d168f70ae8c7d29a436704cbd56
...

diff -r b3af75843235 -r 3f05571385df automaton-in-agda/src/derive.agda
--- a/automaton-in-agda/src/derive.agda	Mon Jul 24 10:10:44 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Mon Jul 24 11:18:43 2023 +0900
@@ -187,7 +187,7 @@
     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 || 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
@@ -198,16 +198,34 @@
      &next : (r y : Regex Σ) → (x : ISB r) → ISBn y → rank y < rank (ISB.s x) → ISBn (y & ISB.s x )
 
 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 ?
+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) = ?
 
 toSB : (r : Regex   Σ) →  ISBn r → Bool
 toSB .(y & ISB.s x) (&next r y x is x₁) = false