Mercurial > hg > Members > kono > Proof > automaton

changeset 94:7c326a484103

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 10 Nov 2019 20:02:36 +0900
parents cdf8ff15efc5
children 86d390666078
files agda/regular-language.agda
diffstat 1 files changed, 20 insertions(+), 12 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Sun Nov 10 18:47:06 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 20:02:36 2019 +0900
@@ -284,25 +284,33 @@
     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 : List Σ → Bool ) → split fa (contain B) x ≡ true
-    lemma13 [] nq fn qa qat fa = ?
-    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 (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)) 
+          → 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
+        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) 
 
     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) (astart A))
+    lemma10 CC = lemma13 x (Concat-NFA-start A B ) CC (astart A) (equal?-refl finab) 
 
     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
     ... | CC = lemma10 CC
 
-    -- AB→split (accept (automaton A) {!!} ) (accept (automaton B) {!!} ) {!!} {!!} {!!} {!!}