Mercurial > hg > Members > kono > Proof > automaton

changeset 97:c1282e442d28

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 13:00:45 +0900
parents 3d362c31b97e
children f196e739b4bf
files agda/regular-language.agda
diffstat 1 files changed, 5 insertions(+), 3 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Mon Nov 11 12:23:43 2019 +0900
+++ b/agda/regular-language.agda	Mon Nov 11 13:00:45 2019 +0900
@@ -296,10 +296,9 @@
         lemma11 : (q : states A ∨ states B)
             → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true
             → q ≡ case1 (δ (automaton A) qa h)
-        lemma11 q ex = lemma17 (subst (λ k → exists finab (λ qn → k qn ) ≡ true ) (f-extensionality finab (λ qn → sym (lemma19 qn) )) ex ) where
-            lemma19 = λ qn → cong ( λ k → nq qn /\ Nδ NFA k h q ) (sym ( qa=q qn (bool-∧→tt-0 {!!} ) )) 
+        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 = {!!}
+            lemma17 en = {!!}
             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
@@ -308,6 +307,9 @@
                ≡⟨  eq ⟩
                   true
                ∎  where open ≡-Reasoning
+            lemma19 : exists finab (λ qn → nq qn /\ Nδ NFA (case1 qa) h q) ≡ true
+            lemma19 = found finab fq ( (lemma18 fq (found-p ( found← finab ex )))) where
+                fq = found-q ( found← finab ex )
 
         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) lemma11