# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573369955 -32400
# Node ID cefa1fa3ee08a4e15cf180a35982061de371fa84
# Parent  e919e82e95a264a1265b8b5e9b6418d4c78a8a41
...

diff -r e919e82e95a2 -r cefa1fa3ee08 agda/regular-language.agda
--- a/agda/regular-language.agda	Sun Nov 10 12:21:44 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 16:12:35 2019 +0900
@@ -281,16 +281,29 @@
          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 x [] refl q nq nqt CC = {!!}
-    lemma11 [] (hz ∷ t) {z} refl q nq nqt CC =
-      lemma11 ([] ++ [ hz ] ) t {z} refl {!!} {!!} {!!} {!!}
-    lemma11 (h ∷ t) (hz ∷ tz) {z} refl q nq nqt CC =
-      lemma11 ((h ∷ t) ++ [ hz ] ) tz {z} (++-assoc (h ∷ t) _ _) {!!} {!!} {!!} {!!}
+    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) _ _) {!!} {!!} {!!} {!!}
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 = {!!}
+    lemma10 CC = lemma11 x [] {x} {!!} {!!} {!!} {!!} CC
 
     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