# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573953665 -32400
# Node ID 5431d94a4c82f7bf1a6b98fa5701d0b2a85be297
# Parent  29e0d2934a0b9b29b3fc56962dca8853e2759c77
...

diff -r 29e0d2934a0b -r 5431d94a4c82 agda/regular-language.agda
--- a/agda/regular-language.agda	Sat Nov 16 21:47:12 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 17 10:21:05 2019 +0900
@@ -301,10 +301,21 @@
     ... | yes eq = bool-or-41 eq
     ... | 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 = {!!}
+       lemma11 q ex with found← finab ex 
+       ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) | q 
+       ... | case1 qa | record { eq = refl } | refl | case1 qa' = lemma14 where
+           lemma15 : q ≡ case1 qa' → nq (case1 qa) /\ Concat-NFA.δnfa A B (case1 qa) h (case1 qa') ≡ true 
+           lemma15 refl = found-p S
+           lemma14 : qa' ≡ δ (automaton A) qa h
+           lemma14 = sym ( equal→refl (afin A)  ( bool-∧→tt-1 (lemma15 {!!} ) ) )
+       ... | case1 qa | record { eq = refl } | refl | case2 qb = {!!} where
+       ... | case2 qb | record { eq = refl } | ab | case1 qa' = {!!} where
+           lemma12 : exists (afin B) (λ qb₁ → accept (automaton B) qb₁ (h ∷ t)) ≡ true → ⊥
+           lemma12 = ab
+       ... | case2 qb | record { eq = refl } | ab | case2 qb' = {!!} where
+           lemma13 : exists (afin B) (λ qb₁ → accept (automaton B) qb₁ (h ∷ t)) ≡ true → ⊥
+           lemma13 = ab
+       
 
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true