--- a/agda/logic.agda	Thu Nov 07 00:17:16 2019 +0900
+++ b/agda/logic.agda	Thu Nov 07 10:55:22 2019 +0900
@@ -78,3 +78,8 @@
 ... | ()
 ≡-Bool-func {false} {false} a→b b→a = refl
 
+bool-≡-? : (a b : Bool) → Dec ( a ≡ b )
+bool-≡-? true true = yes refl
+bool-≡-? true false = no (λ ())
+bool-≡-? false true = no (λ ())
+bool-≡-? false false = yes refl

--- a/agda/regular-language.agda	Thu Nov 07 00:17:16 2019 +0900
+++ b/agda/regular-language.agda	Thu Nov 07 10:55:22 2019 +0900
@@ -4,6 +4,7 @@
 open import Data.List 
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin hiding ( _+_ )
+open import Data.Empty 
 open import Data.Product
 -- open import Data.Maybe
 open import  Relation.Nullary
@@ -173,10 +174,61 @@
     lemma2 [] q qab aA = {!!}
     lemma2 (h ∷ t ) q qab aA  = lemma2 t {!!} {!!} {!!}
 
-split-logic : {Σ : Set} → (A : List Σ → Set )
-      → ( B : List Σ → Set ) → (x :  List Σ ) → Set
-split-logic A B [] = A [] ∧ B []
-split-logic A B (h ∷ t ) = ( A [] ∧ B ( h ∷ t ) ) ∨ split-logic ( λ t1 → A ( h ∷ t1 )) ( λ t2 → B t2 ) t
+record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x :  List Σ ) : Set where
+    field
+        sp0 : List Σ
+        sp1 : List Σ
+        sp-concat : sp0 ++ sp1 ≡ x
+        prop0 : A sp0 ≡ true
+        prop1 : B sp1 ≡ true
+
+open Split
+
+list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
+list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
+list-empty++ [] (x ∷ y) ()
+list-empty++ (x ∷ x₁) y ()
+
+split-next :  {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (h : Σ) (t :  List Σ ) → Split A B (h ∷ t)
+   → ( (A [] ≡ true ) ∧ (B (h ∷ t) ≡ true) ) ∨ Split (λ t1 → A ( h ∷ t1 )) (λ t2 → B t2) t 
+split-next A B h t S with bool-≡-? (A []) true  | bool-≡-? (B (h ∷ t)) true
+split-next A B h t S | yes eqa | yes eqb = case1 (record { proj1 = eqa ; proj2 = eqb })
+split-next A B h t S | yes p | no ¬p with sp0 S
+split-next A B h t S | yes p | no ¬p | [] = {!!} -- ⊥-elim ( ¬p (prop1 S))
+split-next {Σ} A B h t S | yes p | no ¬p | x ∷ tt =
+  case2 record { sp0 = tt ; sp1 = sp1 S ; sp-concat = lemma7 {!!} ; prop0 = lemma8 {!!} ; prop1 = prop1 S } where
+    lemma6 : {ss tt t : List Σ} {h : Σ} → (h ∷ tt ) ++ ss ≡ h ∷ t → tt ++ ss ≡ t
+    lemma6 refl = refl
+    lemma7 : (h ∷ tt ) ++ sp1 S ≡ h ∷ t → tt ++ sp1 S ≡ t
+    lemma7 eq = lemma6 {sp1 S} eq
+    lemma8 :  sp0 S ≡ h ∷ tt → A (h ∷ tt) ≡ true
+    lemma8 refl = prop0 S
+split-next A B h t S | no ¬p | eqb = {!!}
+
+open _∧_
+
+split-logic : {Σ : Set} → (A : List Σ → Bool )
+      → ( B : List Σ → Bool ) → (x :  List Σ ) → Dec (Split A B x)
+split-logic A B [] with bool-≡-? (A []) true  | bool-≡-? (B []) true 
+... | yes eqa | yes eqb  = yes record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
+... | no ne  | _ = no lemma0 where
+    lemma0 : Split A B [] → ⊥
+    lemma0 S with proj1 (list-empty++ (Split.sp0 S)(Split.sp1 S) (Split.sp-concat S))
+    lemma0 S | refl = ne ( Split.prop0 S )
+... | _ | no ne  = no lemma3 where
+    lemma3 : Split A B [] → ⊥
+    lemma3 S with proj2 (list-empty++ (Split.sp0 S)(Split.sp1 S) (Split.sp-concat S))
+    lemma3 S | refl = ne ( Split.prop1 S )
+split-logic A B (h ∷ t ) with split-logic (λ t1 → A (h ∷ t1)) (λ t2 → B t2) t
+... | yes S = yes record { sp0 = h ∷ sp0 S  ; sp1 = sp1 S ; sp-concat = cong ( λ t → h ∷ t) (sp-concat S); prop0 = prop0 S ; prop1 = prop1 S }
+... | no NS with bool-≡-? (A []) true  | bool-≡-? (B (h ∷ t)) true 
+... | yes eqa | yes eqb = yes record { sp0 = [] ; sp1 = (h ∷ t) ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
+... | no ne | _ = no lemma4 where
+    lemma4 :  Split A B (h ∷ t ) → ⊥
+    lemma4 S with sp0 S
+    lemma4 S | [] = ne {!!}
+    lemma4 S | x ∷ tt = NS record { sp0 = [] ; sp1 = t ; sp-concat = refl ; prop0 = {!!} ; prop1 = {!!} }
+... | _ | no ne = no {!!}
 
 
 closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )