Mercurial > hg > Members > kono > Proof > automaton

changeset 90:cefa1fa3ee08

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 16:12:35 +0900
parents e919e82e95a2
children 1bb72cf2af28
files agda/regular-language.agda
diffstat 1 files changed, 19 insertions(+), 6 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Sun Nov 10 12:21:44 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 16:12:35 2019 +0900
@@ -281,16 +281,29 @@
          true
        ∎  where open ≡-Reasoning
 
+    data Next-nq : Set where
+       case-A : { x : List Σ} → ( nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true → Next-nq
+       case-B : { x : List Σ} → ( nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true → Next-nq
+       all-end : Next-nq
+    next-nq : (x : List Σ) → (nq : states A ∨ states B → Bool ) → Naccept NFA finab nq x ≡ true → Next-nq
+    next-nq = {!!}
+
     lemma11 : (x y : List Σ) → {z : List Σ} → x ++ y ≡ z → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
        → Naccept NFA finab nq z ≡ true → split (contain A) (contain B) z ≡ true
-    lemma11 x [] refl q nq nqt CC = {!!}
-    lemma11 [] (hz ∷ t) {z} refl q nq nqt CC =
-      lemma11 ([] ++ [ hz ] ) t {z} refl {!!} {!!} {!!} {!!}
-    lemma11 (h ∷ t) (hz ∷ tz) {z} refl q nq nqt CC =
-      lemma11 ((h ∷ t) ++ [ hz ] ) tz {z} (++-assoc (h ∷ t) _ _) {!!} {!!} {!!} {!!}
+    lemma11 (h ∷ t)  [] {z} refl q nq nqt CC with bool-≡-? (accept (automaton A) (astart A) (h ∷ t)) true  -- first case
+    ... | yes p = AB→split (contain A)  (contain B) (h ∷ t) [] p lemma13 where
+         lemma14 : accept (automaton A) (astart A) (h ∷ t) ≡ true
+         lemma14 = {!!}
+         lemma13 : accept (automaton B) (astart B) [] ≡ true
+         lemma13 = {!!}
+    ... | no ¬p = {!!}
+    lemma11 [] y {z} refl q nq nqt CC = {!!} -- last case
+    lemma11 (h ∷ t) (hz ∷ tz) {z} refl q nq nqt CC with bool-≡-? (aend (automaton A) q) true
+    ... | yes p = lemma11 ((h ∷ t) ++ [ hz ] ) tz {z} (++-assoc (h ∷ t) _ _) {!!} {!!} {!!} {!!}
+    ... | no ¬p = lemma11 ((h ∷ t) ++ [ hz ] ) tz {z} (++-assoc (h ∷ t) _ _) {!!} {!!} {!!} {!!}
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
-    lemma10 = {!!}
+    lemma10 CC = lemma11 x [] {x} {!!} {!!} {!!} {!!} CC
 
     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