Mercurial > hg > Members > kono > Proof > automaton

changeset 280:681df12f0edc

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, 27 Dec 2021 09:51:21 +0900
parents 797fdfe65c93
children 8b437dd616dd
files automaton-in-agda/src/finiteSetUtil.agda automaton-in-agda/src/non-regular.agda
diffstat 2 files changed, 19 insertions(+), 2 deletions(-) [+]
line wrap: on
line diff
--- a/automaton-in-agda/src/finiteSetUtil.agda	Sun Dec 26 18:36:48 2021 +0900
+++ b/automaton-in-agda/src/finiteSetUtil.agda	Mon Dec 27 09:51:21 2021 +0900
@@ -593,7 +593,7 @@
            dup-04 : Dup-in-list (Fin2Finite n) (NList.ls ls1) 
            dup-04 = dup-02 n ls1
            dup-07 : dup-in-list (Fin2Finite (suc n)) (fin+1 (Dup-in-list.dup dup-04)) (NList.ls ls) ≡ true
-           dup-07 = dup-in-list+iso finq {!!} {!!} (dup-in-list+1 {!!} {!!} qs {!!})
+           dup-07 = dup-in-list+iso finq  {!!} {!!} (dup-in-list+1 {!!} {!!} qs {!!})
        ... | case2 dup = record { dup = n1 ; is-dup = dup }
     dup-05 : Q
     dup-05 = Q←F finq (Dup-in-list.dup (dup-02 (finite finq) record { ls = map (F←Q finq) qs ; ls>n = {!!} } ))
--- a/automaton-in-agda/src/non-regular.agda	Sun Dec 26 18:36:48 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Mon Dec 27 09:51:21 2021 +0900
@@ -106,5 +106,22 @@
        tr1 : TA fa tr
        tr1 = tra-phase1 (q₁ ∷ qs) is tr p
 
+open RegularLanguage
+
 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
-lemmaNN r Rg = {!!}
+lemmaNN r Rg = {!!} where
+    n : ℕ
+    n = suc (finite (afin r))
+    nn =  inputnn0 n i0 i1 []
+    nn01  : (i : ℕ) → inputnn1 ( inputnn0 i i0 i1 [] ) ≡ true
+    nn01  = {!!}
+    nn03 : accept (automaton r) (astart r) nn ≡ true
+    nn03 = {!!}
+    nntrace = trace (automaton r) (astart r) nn
+    nn04 :  Trace (automaton r) nn nntrace
+    nn04 = tr-accept← (automaton r) nn (astart r) nn03 
+    nn02 : TA (automaton r) nn04
+    nn02 = tr-append (automaton r) (afin r) (Dup-in-list.dup nn05) _ _ (Dup-in-list.is-dup nn05) nn04 where
+        nn05 : Dup-in-list ( afin r) nntrace
+        nn05 = dup-in-list>n (afin r) nntrace {!!}
+