--- a/agda/regular-language.agda	Tue Nov 12 10:58:01 2019 +0900
+++ b/agda/regular-language.agda	Tue Nov 12 18:54:44 2019 +0900
@@ -5,6 +5,7 @@
 open import Data.Nat hiding ( _≟_ )
 open import Data.Fin hiding ( _+_ )
 open import Data.Empty 
+open import Data.Unit 
 open import Data.Product
 -- open import Data.Maybe
 open import  Relation.Nullary
@@ -281,15 +282,24 @@
 
     open Found
 
-    record run-A : Set (Level.suc Level.zero) where
-       field
-          some : Set
+    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
 
+    open AB-state
     contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
-          → (qa : states A )  → run-A
+          → (qa : states A )  → AB-state nq qa x
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    contain-A [] nq fn qa cond with found← finab fn 
-    ... | S = {!!}
+    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))
+    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
+        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 = {!!}
     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