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

diff -r 7c326a484103 -r 86d390666078 agda/finiteSet.agda
--- a/agda/finiteSet.agda	Sun Nov 10 20:02:36 2019 +0900
+++ b/agda/finiteSet.agda	Mon Nov 11 02:22:02 2019 +0900
@@ -42,6 +42,18 @@
      equal? q0 q1 with F←Q q0 ≟ F←Q q1
      ... | yes p = true
      ... | no ¬p = false
+     equal→refl  : { x y : Q } → equal? x y ≡ true → x ≡ y
+     equal→refl {q0} {q1} eq with F←Q q0 ≟ F←Q q1
+     equal→refl {q0} {q1} refl | yes eq = begin
+            q0
+        ≡⟨ sym ( finiso→ q0) ⟩
+            Q←F (F←Q q0)
+        ≡⟨ cong (λ k → Q←F k ) eq ⟩
+            Q←F (F←Q q1)
+        ≡⟨ finiso→ q1 ⟩
+            q1
+        ∎  where open ≡-Reasoning
+     equal→refl {q0} {q1} () | no ne 
      equal?-refl : {q : Q} → equal? q q ≡ true
      equal?-refl {q} with F←Q q ≟ F←Q q
      ... | yes p = refl
diff -r 7c326a484103 -r 86d390666078 agda/regular-language.agda
--- a/agda/regular-language.agda	Sun Nov 10 20:02:36 2019 +0900
+++ b/agda/regular-language.agda	Mon Nov 11 02:22:02 2019 +0900
@@ -230,8 +230,6 @@
       true
      ∎  where open ≡-Reasoning
 
--- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) already in finiteSet
-
 open NAutomaton
 open import Data.List.Properties
 
@@ -283,29 +281,28 @@
 
     open Found
     lemma13 : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true
-          → (qa : states A ) → ( nq (case1 qa) ≡ true)
+          → (qa : states A ) → ( (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 = {!!} where
-       lemma11 : found-q (found← finab fn) ≡ case1 qa
-       lemma11 = ?
-    
-    -- = {!!} where -- with aend (automaton A) qa | aend (automaton B) (astart B) | found← finab fn
-    --    qe : states A ∨ states B
-    --    qe = found-q (found← finab fn)
-    --    lemma10 : nq qe /\ Nend NFA qe ≡ true
-    --    lemma10 = found-p (found← finab fn)
-    --    lemma11 : aend (automaton A) qa ≡ true
-    --    lemma11 with qe
-    --    lemma11 | case1 qa1 = bool-∧→tt-0 (bool-∧→tt-1 lemma10)
-    --    lemma11 | case2 qb1 = {!!}
-    lemma13 (h ∷ t) nq fn qa qat with aend (automaton A) qa |  accept (automaton B) (δ (automaton B) (astart B) h) t
-    ... | true | true  = refl
-    ... | _ | _ = subst (λ k → _ \/ k ≡ true ) (sym lemma14) bool-or-3 where
+    lemma13 [] nq fn qa qat with found← finab fn 
+    ... | S = lemma16 where
+        lemma15 : (found-q S) ≡ case1 qa 
+        lemma15 = qat (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
+    ... | 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 = {!!}
         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) (nmove (case1 qa) nq qat h) 
+        lemma14 = lemma13 t (Nmoves NFA finab nq h) fn (δ (automaton A) qa 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) (equal?-refl finab) 
+    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) 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 )
 
     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