--- a/agda/regular-language.agda	Sun Nov 10 16:12:35 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 17:39:55 2019 +0900
@@ -281,29 +281,19 @@
          true
        ∎  where open ≡-Reasoning
 
-    data Next-nq : Set where
-       case-A : { x : List Σ} → ( nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true → Next-nq
-       case-B : { x : List Σ} → ( nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true → Next-nq
-       all-end : Next-nq
-    next-nq : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true → Next-nq
-    next-nq = {!!}
-
-    lemma11 : (x y : List Σ) → {z : List Σ} → x ++ y ≡ z → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
-       → Naccept NFA finab nq z ≡ true → split (contain A) (contain B) z ≡ true
-    lemma11 (h ∷ t)  [] {z} refl q nq nqt CC with bool-≡-? (accept (automaton A) (astart A) (h ∷ t)) true  -- first case
-    ... | yes p = AB→split (contain A)  (contain B) (h ∷ t) [] p lemma13 where
-         lemma14 : accept (automaton A) (astart A) (h ∷ t) ≡ true
-         lemma14 = {!!}
-         lemma13 : accept (automaton B) (astart B) [] ≡ true
-         lemma13 = {!!}
-    ... | no ¬p = {!!}
-    lemma11 [] y {z} refl q nq nqt CC = {!!} -- last case
-    lemma11 (h ∷ t) (hz ∷ tz) {z} refl q nq nqt CC with bool-≡-? (aend (automaton A) q) true
-    ... | yes p = lemma11 ((h ∷ t) ++ [ hz ] ) tz {z} (++-assoc (h ∷ t) _ _) {!!} {!!} {!!} {!!}
-    ... | no ¬p = lemma11 ((h ∷ t) ++ [ hz ] ) tz {z} (++-assoc (h ∷ t) _ _) {!!} {!!} {!!} {!!}
+    lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
+          → (qa : states A ) → ( nq (case1 qa) ≡ true)
+          → ( fa : states A → List Σ → Bool ) → split (fa qa) (contain B) x ≡ true
+    lemma13 [] nq fn qa qat fa = AB→split (fa qa) (contain B) [] [] {!!} {!!}
+    lemma13 (h ∷ t) nq fn qa qat fa with fa qa [] | accept (automaton B) (δ (automaton B) (astart B) h) t
+    ... | true | true = refl
+    ... | false | _ = subst (λ k → false \/ k ≡ true ) (sym lemma14 ) (bool-or-1 refl) where
+        lemma14 : split (λ t1 → fa qa (h ∷ t1)) (accept (automaton B) (astart B)) t ≡ true
+        lemma14 = lemma13 t (Nmoves NFA finab nq h) {!!} (δ (automaton A) qa h) {!!} (λ q x → fa qa (h ∷ x)) 
+    ... | _ | false =  {!!}
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = lemma11 x [] {x} {!!} {!!} {!!} {!!} CC
+    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) (accept (automaton A))
 
     closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
     closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C