--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/derive.agda	Wed Nov 28 21:15:49 2018 +0900
@@ -0,0 +1,31 @@
+module derive where
+
+open import nfa
+open import regex1
+open import Data.Nat
+open import Data.List
+
+open import Data.Bool using ( Bool ; true ; false ; _∧_ ; _∨_ )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+
+
+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 = {!!}
+
+
+