--- a/agda/regular-language.agda	Mon Nov 11 21:30:04 2019 +0900
+++ b/agda/regular-language.agda	Tue Nov 12 10:58:01 2019 +0900
@@ -246,7 +246,7 @@
     nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
        exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
     nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q)  h) )  
-    nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) where
+    nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) ) 
     acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true ) 
         → Naccept NFA finab nq z  ≡ true
     acceptB [] q nq nqt fb = lemma8 where
@@ -281,68 +281,21 @@
 
     open Found
 
-    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 )
+    record run-A : Set (Level.suc Level.zero) where
+       field
+          some : Set
 
-    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 )
+    contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
+          → (qa : states A )  → run-A
           → split (accept (automaton A) qa ) (contain B) x ≡ 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
+    contain-A [] nq fn qa cond with found← finab fn 
+    ... | 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) (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
-            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  (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 = {!!}
-                 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 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 {!!}) ⟩
-                  nq qn /\ Nδ NFA qn h q
-               ≡⟨  eq ⟩
-                  true
-               ∎  where open ≡-Reasoning
-            lemma19 : exists finab (λ qn → nq qn /\ Nδ NFA (case1 qa) h q) ≡ true
-            lemma19 = found finab fq ( (lemma18 fq (found-p ( found← finab ex )))) where
-                fq = found-q ( found← finab ex )
-
-        lemma14 : split (λ t1 → accept (automaton A) qa (h ∷ t1)) (contain B) t ≡ true
-        lemma14 = contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11-1
+    ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h)  {!!} ) where
 
     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) (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 ) )
+    lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) {!!} where
 
     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