# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1573442623 -32400
# Node ID 3d362c31b97e8098a0a1308bab9a79266bcf3955
# Parent  86d3906660787cb547dda0a38be069c29f2b775f
...

diff -r 86d390666078 -r 3d362c31b97e agda/regular-language.agda
--- a/agda/regular-language.agda	Mon Nov 11 02:22:02 2019 +0900
+++ b/agda/regular-language.agda	Mon Nov 11 12:23:43 2019 +0900
@@ -281,26 +281,39 @@
 
     open Found
     lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
-          → (qa : states A ) → ( (q : states A ∨ states B) → nq q ≡ true → q ≡ case1 qa )
+          → (qa : states A )  → (nq (case1 qa) ≡ true) → ( (q : states A ∨ states B) → nq q ≡ true → q ≡ case1 qa )
           → split (accept (automaton A) qa ) (contain B) x ≡ true
-    lemma13 [] nq fn qa qat with found← finab fn 
+    lemma13 [] nq fn qa qat qa=q with found← finab fn 
     ... | S = lemma16 where
         lemma15 : (found-q S) ≡ case1 qa 
-        lemma15 = qat (found-q S) (bool-∧→tt-0 (found-p S))
+        lemma15 = qa=q (found-q S) (bool-∧→tt-0 (found-p S))
         lemma16 : aend (automaton A) qa /\ aend (automaton B) (astart B) ≡ true
         lemma16 with lemma15
         ... | refl = bool-∧→tt-1 (found-p S)
-    lemma13 (h ∷ t) nq fn qa qat with bool-≡-? ((aend (automaton A) qa) /\  accept (automaton B) (δ (automaton B) (astart B) h) t ) true
+    lemma13 (h ∷ t) nq fn qa qat qa=q 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 lemma14 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 (case1 qa') eq = {!!}
-        lemma11 (case2 qb) eq = {!!}
+        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 (subst (λ k → exists finab (λ qn → k qn ) ≡ true ) (f-extensionality finab (λ qn → sym (lemma19 qn) )) ex ) where
+            lemma19 = λ qn → cong ( λ k → nq qn /\ Nδ NFA k h q ) (sym ( qa=q qn (bool-∧→tt-0 {!!} ) )) 
+            lemma17 : exists finab (λ qn → nq qn /\ Nδ NFA (case1 qa) h q) ≡ true → q ≡ case1 (δ (automaton A) qa h)
+            lemma17 = {!!}
+            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 ( qa=q qn (bool-∧→tt-0 eq ) )) ⟩
+                  nq qn /\ Nδ NFA qn h q
+               ≡⟨  eq ⟩
+                  true
+               ∎  where open ≡-Reasoning
+
         lemma14 : split (λ t1 → accept (automaton A) qa (h ∷ t1)) (contain B) t ≡ true
-        lemma14 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) lemma11 
+        lemma14 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) (nmove (case1 qa) nq qat h) lemma11 
 
     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) lemma12 where
+    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) lemma12 where
         lemma12 : (q : states A ∨ states B) → Concat-NFA-start A B q ≡ true → q ≡ case1 (astart A)
         lemma12 q eq = sym ( equal→refl finab eq )