--- a/automaton-in-agda/src/derive.agda	Fri Jul 21 12:01:16 2023 +0900
+++ b/automaton-in-agda/src/derive.agda	Sat Jul 22 10:04:39 2023 +0900
@@ -3,7 +3,9 @@
 open import Relation.Binary.PropositionalEquality hiding ( [_] )
 open import Relation.Nullary using (¬_; Dec; yes; no)
 open import Data.List hiding ( [_] )
+open import Data.Empty 
 open import finiteSet
+open import fin
 
 module derive ( Σ : Set) ( fin : FiniteSet Σ ) ( eq? : (x y : Σ) → Dec (x ≡ y)) where
 
@@ -62,20 +64,28 @@
 derive-step r d0 s = derive (is-derived d0) s
 
 regex→automaton : (r : Regex   Σ) → Automaton (Derivative r) Σ
-regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive-step r d s} 
+regex→automaton r = record { δ = λ d s → record { state = derivative (state d) s ; is-derived = derive (is-derived d) s} 
    ; aend = λ d → empty? (state d) }  
 
 regex-match : (r : Regex   Σ) →  (List Σ) → Bool
 regex-match ex is = accept ( regex→automaton ex ) record { state =  ex ; is-derived = unit } is 
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
+
+D-cong :  (r s : Regex Σ) → (x : Derivative r) (y : Derivative s) 
+   → state x ≡ state y → is-derived x ≅ is-derived y  → x ≅ y
+D-cong = ?
+
+D-inject :  (r : Regex Σ) → {x y : Derivative r} → x ≡ y
+D-inject r {x} {y} = HE.≅-to-≡  (D-cong r r x y ? ? )
+
 -- open import nfa
 open import Data.Nat
--- open import Data.Nat hiding ( _<_ ; _>_ )
--- open import Data.Fin hiding ( _<_ )
+open import Data.Nat.Properties
 open import nat
 open import finiteSetUtil
 open FiniteSet
-open import Data.Fin hiding (_<_)
+open import Data.Fin hiding (_<_ ; _≤_ ; pred )
 
 -- finiteness of derivative 
 --    term generate   x & y   for each * and & only once
@@ -101,30 +111,28 @@
     sb* : (x : Regex Σ) → (xn : ℕ) → SB x xn  → SB (x *) (suc xn)
     sb& : (x y : Regex Σ) → (xn yn : ℕ) → xn < yn  → ( sx : SB x xn ) (sy : SB y yn ) → SB (x & y) (suc yn)
 
-sb-id : (r : Regex Σ) → SB r (rank r) → Bool
-sb-id r sb with rank r | inspect rank r
-sb-id ε sbε | zero | _ = true
-sb-id φ sbφ | zero | _ = true
-sb-id < t > (sb<> s) | zero | _ with eq? t s
-... | yes _ = true
-... | no _  = false
-sb-id (x0 || y0) (sb| x y xn yn .zero sb sb₁ x₁) | zero | record { eq = eq1 } = sb-id x0 ?  /\ sb-id y0 ?  
-sb-id _ (sb| x y xn yn .(suc k) sb sb₁ x₁) | suc k | record { eq = eq1 } = sb-id x ?  /\ sb-id y ?  
-sb-id (y *) (sb* x t u) | suc k | record{ eq = eq1 } = sb-id y ?
-sb-id (x0 & y0) (sb& .x0 .y0 xn .k x z z₁) | suc k | record { eq = eq1 } = sb-id x0 ? /\ sb-id y0 ?
-
 open import bijection using ( InjectiveF ; Is )  
 
 finSBTA : (r : Regex Σ) → FiniteSet (SB r (rank r) → Bool)
-finSBTA r = fin→ ( fb00 (rank r) r refl ) where
-    fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≡ n → FiniteSet (SB r (rank r))
-    fb00 zero ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? }
-    fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = ? ; finiso← = ? }
+finSBTA r = fin→ ( fb00 (rank r) r ≤-refl ) where
+    fb00 : (n : ℕ ) → (r : Regex Σ) → rank r ≤ n → FiniteSet (SB r (rank r))
+    fb00 n ε eq = record { finite = 1 ; Q←F = λ _ → sbε ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0  } where
+        fb01 :  (q : SB ε 0) → sbε ≡ q
+        fb01 sbε = refl
+    fb00 zero φ eq = record { finite = 1 ; Q←F = λ _ → sbφ ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
+        fb01 :  (q : SB φ 0) → sbφ ≡ q
+        fb01 sbφ = refl
     fb00 zero (r || r₁) eq = iso-fin (fin-∨ (fb00 zero r ?) (fb00 zero r₁ ?)) ?
-    fb00 zero < x > eq = iso-fin fin ?
+    fb00 zero < x > eq = record { finite = 1 ; Q←F = λ _ → sb<> x ; F←Q = λ _ → # 0 ; finiso→ = fb01 ; finiso← = fin1≡0 } where
+        fb01 : (q : SB < x > 0) → sb<> x ≡ q
+        fb01 (sb<> x) = refl
     fb00 (suc n) (r *) eq = iso-fin (fb00 n r ?) ?
     fb00 (suc n) (r & r₁) eq = iso-fin (fin-∧ (fb00 n r ?) (fb00 n r₁ ?)) ?
-    fb00 (suc n) (r || r₁) eq = iso-fin (fin-∧ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ?
+    fb00 (suc n) (r || r₁) eq = iso-fin (fin-∨ (fb00 (suc n) r ?) (fb00 (suc n) r₁ ?)) ?
+    fb00 zero (x *) ()
+    fb00 zero (x & x₁) ()
+    fb00 (suc n) φ z≤n =  fb00 n φ z≤n 
+    fb00 (suc n) < x > z≤n = fb00 n < x > z≤n 
 
 record SBf (r : Regex Σ) (n : ℕ) : Set where
     field
@@ -146,8 +154,13 @@
     ... | false | record { eq = eq1} = no (λ n → ¬-bool {a sbε} eq1 (fl04 n)) where
          fl04 : Is (Derivative ε) (SB ε 0 → Bool) fb02 a → a sbε ≡ true
          fl04 n = sym (cong (λ k → k sbε) (Is.fa=c n))
+    fl06 :  (y : Regex Σ) → (s : Σ) → ¬ ( regex-states y ε )
+    fl06 y s x with derivative y s | inspect (derivative y) s
+    ... | d | record { eq = eq1 } = ?
     fl05 :  {x y : Derivative ε} → fb02 x ≡ fb02 y → x ≡ y
-    fl05 {x} {y} eq = ?
+    fl05 {x} {y} eq with is-derived x | inspect is-derived x 
+    ... | unit | record { eq = eq1 } = ?
+    ... | derive e s | record { eq = eq1 } = ?
 SBN φ = ?
 SBN (r *) = ?
 SBN (r & r₁) = record { rank=n = ? ; f = ? ; sb-inject = ? ; dec = ? }

--- a/automaton-in-agda/src/fin.agda	Fri Jul 21 12:01:16 2023 +0900
+++ b/automaton-in-agda/src/fin.agda	Sat Jul 22 10:04:39 2023 +0900
@@ -51,6 +51,9 @@
 
 open import Data.Nat.Properties as NatP  hiding ( _≟_ )
 
+fin1≡0 : (f : Fin 1) → # 0 ≡ f
+fin1≡0 zero = refl
+
 fin+1≤ : { i n : ℕ } → (a : i < n)  → fin+1 (fromℕ< a) ≡ fromℕ< (<-trans a a<sa)
 fin+1≤ {0} {suc i} (s≤s z≤n) = refl
 fin+1≤ {suc n} {suc (suc i)} (s≤s (s≤s a)) = cong (λ k → suc k ) ( fin+1≤ {n} {suc i} (s≤s a) )