# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640566281 -32400
# Node ID 681df12f0edc626873bd4b26ae505ed93041af0d
# Parent  797fdfe65c9306077c132620bf4db3accd115f31
...

diff -r 797fdfe65c93 -r 681df12f0edc automaton-in-agda/src/finiteSetUtil.agda
--- 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 = {!!} } ))
diff -r 797fdfe65c93 -r 681df12f0edc automaton-in-agda/src/non-regular.agda
--- 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 {!!}
+