--- a/agda/derive.agda	Sat Dec 22 11:45:37 2018 +0900
+++ b/agda/derive.agda	Sat Dec 22 15:48:05 2018 +0900
@@ -35,116 +35,20 @@
        finiso←' (suc (suc ()))
 
 
-test-r1 = < i0 > & < i1 >
-test-r2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
-test-r3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
+tr1 = < i0 > & < i1 >
+tr2 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i1  ∷ [] )
+tr3 = regular-language (< i0 > & < i1 >) finIn2 ( i0  ∷ i0  ∷ [] )
+tr4 = (< i0 > * ) & < i1 >
+tr5 = ( ((< i0 > * ) & < i1 > ) || ( < i1 > & ( ( < i1 > * ) || ( < i0 > * )) ) ) *
 
-issub : {Σ : Set} {n : ℕ } → Regex Σ → Regex Σ → FiniteSet Σ {n} → Bool
-issub (r *) s f = issub r s f
-issub (r & r₁) s f = issub r s f ∨ issub r₁ s f
-issub (r || r₁) s f =  issub r s f ∨ issub r₁ s f
-issub < x > < s > f with cmpi f x s 
-issub < x > < s > f | yes p = true
-issub < x > < s > f | no ¬p = false
-issub < x > s f  = false
-
-record RegexSub {Σ : Set} (R :  Regex Σ) {n : ℕ }  (fin :  FiniteSet Σ {n} ): Set where
-    field
-       Subterm : Regex Σ
-       sub     : issub R Subterm fin ≡ true
-
-open import Data.Product
+sb : { Σ : Set } → Regex Σ → List ( Regex Σ )
+sb (x *) =  map (λ r → ( r & (x *) )) ( sb x ) ++ ( sb x ) 
+sb (x & y) = map (λ r → ( r & y )) ( sb x ) ++ ( sb y ) 
+sb (x || y) = sb x ++ sb y 
+sb < x > = < x >  ∷ []
 
 
-regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) 
-regex2nfa {Σ} (r *) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!}  where
-          nr0 =  proj₁ (regex2nfa r fin)
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
-          Nstart : (Regex Σ) → Bool
-          Nstart s0 = NAutomaton.Nstart nr0 s0
-          Nend : (Regex Σ) → Bool
-          Nend s0 =  NAutomaton.Nend nr0 s0
-regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
-          nr0 =  proj₁ (regex2nfa r0 fin)
-          nr1 =  proj₁ (regex2nfa r1 fin)
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧  NAutomaton.Nδ nr1 s0 i s1 )
-          Nstart : (Regex Σ) → Bool
-          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
-          Nend : (Regex Σ) → Bool
-          Nend s0 = NAutomaton.Nend nr0 s0  ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
-regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
-          nr0 =  proj₁ (regex2nfa r0 fin)
-          nr1 =  proj₁ (regex2nfa r1 fin)
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
-          Nstart : (Regex Σ) → Bool
-          Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ NAutomaton.Nstart nr1 s0 
-          Nend : (Regex Σ) → Bool
-          Nend s0 = NAutomaton.Nend nr0 s0  ∨ NAutomaton.Nend nr1 s0 
-regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
-          Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
-          Nδ r1 s r2 with cmpi fin s x
-          Nδ r1 s r2 | yes _ = true
-          Nδ r1 s r2 | no _ = false
-          Nstart : (Regex Σ) → Bool
-          Nstart = {!!}
-          Nstart < s > with cmpi fin s x
-          ... | yes _ = true
-          ... | no  _ = false
-          Nstart _ = false
-          Nend  :  (Regex Σ) → Bool
-          Nend  _ = false
-
-test-r4 = regex2nfa  (< i0 > & < i1 >) finIn2 
-
-testr5 = Naccept ( proj₁ test-r4) {!!} ( i0  ∷ i1  ∷ [] )
-
-rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s } 
-rfin {Σ} s = record {
-        Q←F = Q←F'
-      ; F←Q  = F←Q'
-      ; finiso→ = finiso→'
-      ; finiso← = finiso←'
-  } where
-        Q←F' : Fin (length s) → Regex Σ
-        Q←F' = {!!}
-        F←Q'  : Regex Σ → Fin (length s)
-        F←Q'  = {!!}
-        finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q
-        finiso→' = {!!}
-        finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f
-        finiso←' = {!!}
-
-reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) 
-     → ( regex : Regex Σ )
-     → ( In : List Σ )
-     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} (  proj₁ ( regex2nfa {Σ} regex  fin  ))
-         (rfin (proj₂  ( regex2nfa {Σ} regex  fin  ) )) In
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!}
-
-
-derivatives : {Σ : Set} → Σ → Regex  Σ → Regex  Σ
-derivatives x (r *) = {!!}
-derivatives x (r & r₁) = {!!}
-derivatives x (r || r₁) = {!!}
-derivatives x < x₁ > = {!!}
-
-daccept : {Σ : Set} → ( r : Regex  Σ ) →  {n : ℕ } (fin : FiniteSet Σ {n}) → ( s :  List Σ ) → Bool
-daccept r fin [] = {!!}
-daccept r fin (h ∷ t) =  regular-language ( derivatives h r ) fin t
-
-lemma1 : {Σ : Set} → ( r : Regex  Σ ) →  {n : ℕ } (fin : FiniteSet Σ {n}) → ( s :  List Σ )
-     → regular-language r fin s ≡ true → daccept r fin s  ≡ true
-lemma1 = {!!}
-
-lemma2 : {Σ : Set} → ( r : Regex  Σ ) →  {n : ℕ } (fin : FiniteSet Σ {n}) → ( s :  List Σ )
-     → daccept r fin s  ≡ true → regular-language r fin s ≡ true 
-lemma2 = {!!}
-
-
-
+nth : { S : Set } → (x : List S ) → Fin ( length x ) → S
+nth [] ()
+nth (s ∷ t) zero = s
+nth (_ ∷ t) (suc f) = nth t f