Mercurial > hg > Members > kono > Proof > automaton

changeset 89:e919e82e95a2

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 12:21:44 +0900
parents e7b3a2856ccb
children cefa1fa3ee08
files agda/regular-language.agda
diffstat 1 files changed, 8 insertions(+), 8 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Sun Nov 10 10:55:25 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 10 12:21:44 2019 +0900
@@ -123,10 +123,6 @@
        nend (case2 q) = aend (automaton B) q
        nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case
 
--- Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
--- Concat-NFA-start A B (case1 q) = equal? (afin A) q (astart A)
--- Concat-NFA-start _ _ _ = false
-
 Concat-NFA-start :  {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
 Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q
 
@@ -237,6 +233,7 @@
 -- postulate f-extensionality : { n : Level}  → Relation.Binary.PropositionalEquality.Extensionality n n -- (Level.suc n) already in finiteSet
 
 open NAutomaton
+open import Data.List.Properties
 
 closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
@@ -284,10 +281,13 @@
          true
        ∎  where open ≡-Reasoning
 
-    lemma11 : (x y : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
-       → split (contain A) (contain B) (x ++ y) ≡ true
-    lemma11 x [] q nq nqt = {!!}
-    lemma11 x (h ∷ t) q nq nqt = {!!}
+    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) _ _) {!!} {!!} {!!} {!!}
 
     lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x  ≡ true → split (contain A) (contain B) x ≡ true
     lemma10 = {!!}