--- a/agda/regular-language.agda	Mon Nov 11 14:25:42 2019 +0900
+++ b/agda/regular-language.agda	Mon Nov 11 21:30:04 2019 +0900
@@ -280,38 +280,54 @@
        ∎  where open ≡-Reasoning
 
     open Found
-    lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
-          → (qa : states A )  → (nq (case1 qa) ≡ true) → ( (q : states A ∨ states B) → nq q ≡ true → q ≡ case1 qa )
+
+    contain-B : ( h : Σ) → ( t : List Σ ) → ( nq : states A ∨ states B → Bool ) → (qb : states B) → ( nq (case2 qb) ≡ true ) →
+       Naccept NFA finab nq (h ∷ t) ≡ true → accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
+    contain-B = {!!}
+
+    condition-A : (nq :  states A ∨ states B → Bool ) → (qa : states A) → (q : states A ∨ states B) → Set
+    condition-A nq qa q =  ( nq q  ≡ true → q ≡ case1 qa ) ∨ ( (nq (case1 qa) /\ aend (automaton A) qa /\ nq (case2 (astart B))) ≡ true )
+
+    contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
+          → (qa : states A )  → (nq (case1 qa) ≡ true) → ( (q :  states A ∨ states B ) → condition-A nq qa q )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    lemma13 [] nq fn qa qat qa=q with found← finab fn 
-    ... | S = lemma16 where
-        lemma15 : (found-q S) ≡ case1 qa 
-        lemma15 = qa=q (found-q S) (bool-∧→tt-0 (found-p S))
-        lemma16 : aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true
-        lemma16 with lemma15
-        ... | refl = bool-∧→tt-1 (found-p S)
-    lemma13 (h ∷ t) nq fn qa qat qa=q with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
+    contain-A [] nq fn qa qat cond with found← finab fn 
+    ... | S with cond (found-q S)
+    ... | case2 end = {!!}
+    ... | case1 qa=q with qa=q (bool-∧→tt-0 (found-p S))
+    ... | refl = bool-∧→tt-1 (found-p S)
+    contain-A (h ∷ t) nq fn qa qat cond with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
     ... | yes eq = bool-or-41 eq
-    ... | no ne = bool-or-31 lemma14 where
-        lemma11 : (q : states A ∨ states B)
+    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11-1 ) where
+        lemma11-1 : (q : states A ∨ states B)  → condition-A (λ q → exists finab (λ qn → nq qn /\ Nδ NFA qn h q)) (δ (automaton A) qa h) q
+        lemma11-1 q with cond q
+        ... | case2 end = {!!}
+        ... | case1 qa=q = case1 (lemma11 q) where
+         lemma11 : (q : states A ∨ states B)
             → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true
             → q ≡ case1 (δ (automaton A) qa h)
-        lemma11 q ex = lemma17 lemma19 where
+         lemma11 q ex = lemma17 lemma19 where
             lemma17 : exists finab (λ qn → nq qn /\ Nδ NFA (case1 qa) h q) ≡ true → q ≡ case1 (δ (automaton A) qa h)
             lemma17 en with found← finab en 
-            ... | S with found-q S | found-p S | qa=q (found-q S) (bool-∧→tt-0 ( found-p S))
-            ... | (case1 qq) | e1 | refl =  lemma21 q refl where
+            ... | S with found-q S | found-p S | {!!} -- qa=q  (bool-∧→tt-0 ( found-p S))(found-q S)
+            ... | (case1 qq) | e1 | eq =  lemma21 q refl where
                  lemma20 : nq (case1 qa) /\ Concat-NFA.δnfa A B (case1 qa) h q ≡ true
-                 lemma20 = e1
+                 lemma20 = {!!}
                  lemma21 : (qq : states A ∨ states B) → qq ≡ q → q ≡ case1 (δ (automaton A) qa h)
                  lemma21 (case1 x) refl = cong ( λ k → case1 k ) (sym lemma23 ) where
                      lemma23 : (δ (automaton A) qa h) ≡ x
                      lemma23 = equal→refl (afin A) ( bool-∧→tt-1 e1)
-                 lemma21 (case2 x) refl = {!!} -- ⊥-elim (ne (bool-∧→tt-1  e1))
+                 lemma21 (case2 x) refl with bool-≡-? (aend (automaton A) qa) true
+                 ... | no not1 = ⊥-elim ( not1 ( bool-∧→tt-0 ( bool-∧→tt-1 e1)))
+                 ... | yes a-end = ⊥-elim ( ne (bool-and-tt a-end lemma25 ) ) where
+                     lemma24 : aend (automaton A) qa /\ (equal? (afin B) x (δ (automaton B) (astart B) h)) ≡ true
+                     lemma24 = bool-∧→tt-1 e1
+                     lemma25 : accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true
+                     lemma25 =  contain-B h t nq (astart B) {!!} fn
             lemma18 : (qn :  states A ∨ states B) → nq qn /\ Nδ NFA qn h q ≡ true → nq qn /\ Nδ NFA (case1 qa) h q ≡ true
             lemma18 qn eq = begin
                   nq qn /\ Nδ NFA (case1 qa) h q
-               ≡⟨ cong ( λ k → nq qn /\ Nδ NFA k h q ) (sym ( qa=q qn (bool-∧→tt-0 eq ) )) ⟩
+               ≡⟨ cong ( λ k → nq qn /\ Nδ NFA k h q ) (sym {!!}) ⟩
                   nq qn /\ Nδ NFA qn h q
                ≡⟨  eq ⟩
                   true
@@ -321,12 +337,12 @@
                 fq = found-q ( found← finab ex )
 
         lemma14 : split (λ t1 → accept (automaton A) qa (h ∷ t1)) (contain B) t ≡ true
-        lemma14 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11 
+        lemma14 = contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11-1
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) lemma12 where
-        lemma12 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → q ≡ case1 (astart A)
-        lemma12 q eq = sym ( equal→refl finab eq )
+    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) lemma12-1 where
+        lemma12-1 : (q : states A ∨ states B) → condition-A (Concat-NFA-start A B) (astart A) q
+        lemma12-1 q = case1 (λ eq → sym ( equal→refl finab eq ) )
 
     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