--- a/agda/regular-language.agda	Wed Nov 13 07:50:31 2019 +0900
+++ b/agda/regular-language.agda	Wed Nov 13 09:04:48 2019 +0900
@@ -285,7 +285,9 @@
     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 ) →
-           ( (q ≡ case1 qa)  ∨ ({qb : states B} → nq (case2 qb) ≡ true →   ( accept (automaton B) qb x ≡ false ) )))  → AB-state nq qa x
+           ( (q ≡ case1 qa)  ∨
+           ( ({ qa' : states A} → (¬ (q ≡ case1 qa'))) ∧ ({qb : states B} → nq (case2 qb) ≡ true →   ( accept (automaton B) qb x ≡ false ) ))))
+           → AB-state nq qa x
 
     open AB-state
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
@@ -294,12 +296,12 @@
     contain-A [] nq fn qa cond with found← finab fn | found-q (found← finab fn) | cond | inspect found-q (found← finab fn)
     contain-A [] nq fn qa cond | S | s | state-A nq=t | record { eq = refl }  with  nq=t (found-q S) (bool-∧→tt-0 (found-p S))
     ... | refl  = bool-∧→tt-1 (found-p S)
-    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S)) | inspect (cond-b (found-q S)) (bool-∧→tt-0 (found-p S))
-    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ | case1 refl | _ =  bool-∧→tt-1 (found-p S)
-    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | case2 accept-B | _ = ⊥-elim ( lemma11 accept-B )  where
+    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S)) 
+    contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ | case1 refl =  bool-∧→tt-1 (found-p S)
+    contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl }   | case2 accept-B = ⊥-elim ( lemma11 (proj2 accept-B) )  where
         lemma11 :  (  nq (case2 qb ) ≡ true → aend (automaton B) qb ≡ false ) → ⊥
         lemma11  accept-B = ¬-bool ( accept-B (bool-∧→tt-0 (found-p S))) (bool-∧→tt-1 (found-p S ))
-    contain-A [] nq fn qa cond | S | case1 qa' | state-AB cond-b | record { eq = refl }  | case2 accept-B | record { eq = ee} = {!!}
+    contain-A [] nq fn qa cond | S | case1 qa' | state-AB cond-b | record { eq = refl }  | case2 accept-B = ⊥-elim ( (proj1 accept-B ) refl )
     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)  {!!} ) where