Mercurial > hg > Members > kono > Proof > automaton

changeset 98:f196e739b4bf

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 Mon, 11 Nov 2019 14:25:42 +0900
parents c1282e442d28
children aca3f1349913
files agda/regular-language.agda
diffstat 1 files changed, 10 insertions(+), 1 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Mon Nov 11 13:00:45 2019 +0900
+++ b/agda/regular-language.agda	Mon Nov 11 14:25:42 2019 +0900
@@ -298,7 +298,16 @@
             → q ≡ case1 (δ (automaton A) qa h)
         lemma11 q ex = lemma17 lemma19 where
             lemma17 : exists finab (λ qn → nq qn /\ Nδ NFA (case1 qa) h q) ≡ true → q ≡ case1 (δ (automaton A) qa h)
-            lemma17 en = {!!}
+            lemma17 en with found← finab en 
+            ... | S with found-q S | found-p S | qa=q (found-q S) (bool-∧→tt-0 ( found-p S))
+            ... | (case1 qq) | e1 | refl =  lemma21 q refl where
+                 lemma20 : nq (case1 qa) /\ Concat-NFA.δnfa A B (case1 qa) h q ≡ true
+                 lemma20 = e1
+                 lemma21 : (qq : states A ∨ states B) → qq ≡ q → q ≡ case1 (δ (automaton A) qa h)
+                 lemma21 (case1 x) refl = cong ( λ k → case1 k ) (sym lemma23 ) where
+                     lemma23 : (δ (automaton A) qa h) ≡ x
+                     lemma23 = equal→refl (afin A) ( bool-∧→tt-1 e1)
+                 lemma21 (case2 x) refl = {!!} -- ⊥-elim (ne (bool-∧→tt-1  e1))
             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