--- a/agda/regular-language.agda	Fri Nov 15 11:51:31 2019 +0900
+++ b/agda/regular-language.agda	Sat Nov 16 21:47:12 2019 +0900
@@ -282,46 +282,36 @@
 
     open Found
 
-    ab-case : (q : states A ∨ states B ) → (x : List Σ ) → Set
-    ab-case (case1 qa) x = (qa' : states A ) → qa'  ≡ qa
-    ab-case (case2 qb) x = ¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true )
-
-    data AB-state (nq : states A ∨ states B → Bool ) (qa : states A) (x : List Σ) :  Set (Level.suc Level.zero) where
-       state-A  : ((q : states A ∨ states B ) → nq q ≡ true → q ≡ case1 qa ) → AB-state nq qa x
-       state-AB : ((q : states A ∨ states B ) → nq q ≡ true → ab-case q x ) → AB-state nq qa x
-
-    open AB-state
+    ab-case : (q : states A ∨ states B ) → (qa : states A ) → (x : List Σ ) → Set
+    ab-case (case1 qa') qa x = qa'  ≡ qa
+    ab-case (case2 qb) qa x = ¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true )
 
     start-eq  : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → exists (afin A) (λ qa → equal? finab q (case1 qa)) ≡ true
     start-eq q eq with equal→refl finab eq
     ... | refl =  found (afin A) (astart A) eq
 
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
-          → (qa : states A )  → AB-state nq qa x
+          → (qa : states A )  → (  (q : states A ∨ states B) → nq q ≡ true → ab-case q qa x )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    contain-A [] nq fn qa (state-A caseA) with found← finab fn 
-    ... | S with found-q S | caseA (found-q S) (bool-∧→tt-0 (found-p S)) 
-    ... | case2 qb | ()
-    ... | case1 qa | refl = lemma11 (caseA (found-q S) (bool-∧→tt-0 (found-p S))) (bool-∧→tt-1 (found-p S)) where
-         lemma11 : found-q S ≡ case1 qa → Concat-NFA.nend A B (found-q S) ≡ true → aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true
-         lemma11 refl xx = xx
-    contain-A [] nq fn qa (state-AB caseAB) with found← finab fn 
-    ... | S with found-q S | inspect found-q S | caseAB (found-q S) (bool-∧→tt-0 (found-p S))
-    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (found (afin B) qb (bool-∧→tt-1 (found-p S)) )) where
-    ... | case1 qa' | record { eq = refl } | ab with ab qa
-    ... | refl = bool-∧→tt-1 (found-p S) 
+    contain-A [] nq fn qa cond with found← finab fn 
+    ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
+    ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (found (afin B) qb (bool-∧→tt-1 (found-p S)) )) 
+    ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
     contain-A (h ∷ t) nq fn qa 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 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma12 ) where
-       lemma13 : (q : states A ∨ states B ) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true
-           → (q ≡ case1 (δ (automaton A) qa h)) ∨ (¬ (exists (afin B) (λ qb → accept (automaton B) qb x ) ≡ true ))
-       lemma13 (case1 qa') ex = case1 {!!}
-       lemma13 (case2 qb) ex = case2 ?
-       lemma12 : AB-state (λ q → exists finab (λ qn → nq qn /\ Nδ NFA qn h q))  (δ (automaton A) qa h) t
-       lemma12 = state-A ( λ q ex → {!!} ) 
+    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 ) where
+       lemma11 :  (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
+       lemma11 (case1 qa' ) ex with cond (case1 qa')  {!!} | found← finab ex
+       ... | exex | E = {!!}
+       lemma11 (case2 qb ) ex with cond (case2 qb)  {!!} | found← finab ex
+       ... | exex | E = {!!}
+
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) (state-A ( λ qa nq=t → {!!} ))
+    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) lemma15 where 
+       lemma15 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → ab-case q (astart A) x
+       lemma15 q nq=t with equal→refl finab nq=t 
+       ... | refl = refl
 
     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