# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573376870 -32400
# Node ID b1bc0802d774749361f15ad40fccfd6bf178b910
# Parent  1bb72cf2af28370c12ebf95e4435bea71c3f6ad0
...

diff -r 1bb72cf2af28 -r b1bc0802d774 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 10 17:39:55 2019 +0900
+++ b/agda/finiteSet.agda	Sun Nov 10 18:07:50 2019 +0900
@@ -15,8 +15,8 @@
 
 record Found ( Q : Set ) (p : Q → Bool ) : Set where
      field
-       found : Q
-       found-p : p found ≡ true
+       found-q : Q
+       found-p : p found-q ≡ true
 
 record FiniteSet ( Q : Set ) { n : ℕ } : Set  where
      field
@@ -100,7 +100,7 @@
              lemma : (λ z → p (Q←F (F←Q z))) ≡ p
              lemma = f-extensionality ( λ q → subst (λ k → p k ≡ p q ) (sym (finiso→ q)) refl )
          found2 (suc m)  m<n end with bool-≡-? (p (Q←F (fromℕ≤ m<n))) true
-         found2 (suc m)  m<n end | yes eq = record { found = Q←F (fromℕ≤ m<n) ; found-p = eq }
+         found2 (suc m)  m<n end | yes eq = record { found-q = Q←F (fromℕ≤ m<n) ; found-p = eq }
          found2 (suc m)  m<n end | no np = 
                found2 m (lt2 m<n) (next-end p end m<n (¬-bool-t np )) 
      not-found← : { p : Q → Bool } → exists p ≡ false → (q : Q ) → p q ≡ false 
diff -r 1bb72cf2af28 -r b1bc0802d774 agda/regular-language.agda
--- a/agda/regular-language.agda	Sun Nov 10 17:39:55 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 18:07:50 2019 +0900
@@ -281,19 +281,26 @@
          true
        ∎  where open ≡-Reasoning
 
+    open Found
     lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
           → (qa : states A ) → ( nq (case1 qa) ≡ true)
-          → ( fa : states A → List Σ → Bool ) → split (fa qa) (contain B) x ≡ true
-    lemma13 [] nq fn qa qat fa = AB→split (fa qa) (contain B) [] [] {!!} {!!}
-    lemma13 (h ∷ t) nq fn qa qat fa with fa qa [] | accept (automaton B) (δ (automaton B) (astart B) h) t
+          → ( fa : List Σ → Bool ) → split fa (contain B) x ≡ true
+    lemma13 [] nq fn qa qat fa with found← finab fn
+    ... | S = {!!} where
+        lemma16 : nq (found-q S) /\ Concat-NFA.nend A B (found-q S) ≡ true
+        lemma16 = found-p S
+    -- = AB→split fa (contain B) [] [] {!!} {!!}
+    lemma13 (h ∷ t) nq fn qa qat fa with fa [] | accept (automaton B) (δ (automaton B) (astart B) h) t
     ... | true | true = refl
     ... | false | _ = subst (λ k → false \/ k ≡ true ) (sym lemma14 ) (bool-or-1 refl) where
-        lemma14 : split (λ t1 → fa qa (h ∷ t1)) (accept (automaton B) (astart B)) t ≡ true
-        lemma14 = lemma13 t (Nmoves NFA finab nq h) {!!} (δ (automaton A) qa h) {!!} (λ q x → fa qa (h ∷ x)) 
-    ... | _ | false =  {!!}
+        lemma14 : split (λ t1 → fa (h ∷ t1)) (accept (automaton B) (astart B)) t ≡ true
+        lemma14 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) (λ x → fa (h ∷ x)) 
+    ... | _ | false = subst (λ k → (_ /\ false) \/ k ≡ true ) (sym lemma15) (bool-or-1 (bool-and-2 refl) ) where
+        lemma15 : split (λ t1 → fa (h ∷ t1)) (accept (automaton B) (astart B)) t ≡ true
+        lemma15 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) (λ x → fa (h ∷ x)) 
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) (accept (automaton A))
+    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) (accept (automaton A) (astart A))
 
     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