# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1641007659 -32400
# Node ID b0a88e0241888050ee5b2c635801f138bfffb35e
# Parent  5261402429f93f416ce20da3c777979d8783caaa
...

diff -r 5261402429f9 -r b0a88e024188 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Sat Jan 01 11:00:41 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sat Jan 01 12:27:39 2022 +0900
@@ -118,6 +118,7 @@
        xyz=is : x ++ y ++ z ≡ is 
        trace-xyz  : Trace fa (x ++ y ++ z)  q
        trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
+       non-nil-y : ¬ (y ≡ [])
 
 open import nat
 
@@ -140,6 +141,7 @@
    tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
           | phase1 finq qd (tr→qs fa is (δ fa q i) tr) | inspect ( phase1 finq qd)  (tr→qs fa is (δ fa q i) tr) 
    ... | true | record { eq = eq } | false | record { eq = np} = record { x = [] ; y = i ∷ TA1.y ta ;  z = TA1.z ta ; xyz=is =  cong (i ∷_ ) (TA1.yz=is ta)
+           ; non-nil-y = λ ()
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
            ; trace-xyyz = tra-02 (i ∷ TA1.y ta) (TA1.z ta) q
                     (tnext q (TA1.trace-yz ta)) (subst (λ k → Trace fa (TA1.z ta)  k) {!!} (TA1.trace-z ta)) {!!} {!!}  } where
@@ -166,10 +168,12 @@
            ... | true | record { eq = eq } = {!!}  -- y2 + z1 contains two qd
            ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qs zqs {!!} {!!} np2 )
    ... | true | record { eq = eq } | true | record { eq = np} = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta)
+           ; non-nil-y = non-nil-y ta
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
         ta : TA fa (δ fa q i ) is
         ta = tra-phase1 (δ fa q i ) is tr np
    ... | false | _ | _ | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta) 
+           ; non-nil-y = non-nil-y ta
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
         ta : TA fa (δ fa q i ) is
         ta = tra-phase1 (δ fa q i ) is tr p
@@ -189,18 +193,12 @@
     ... | t = {!!}
     nn03 : accept (automaton r) (astart r) nn ≡ true
     nn03 = subst (λ k → k ≡ true ) (Rg nn ) (nn01 n)
-    count : In2 → List In2 → ℕ
-    count _ [] = 0
-    count i0 (i0 ∷ s) = suc (count i0 s)
-    count i1 (i1 ∷ s) = suc (count i1 s)
-    count x (_ ∷ s) = count x s
-    nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
-    nn10 = {!!}
-    nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
-    nn11 = {!!}
-    nntrace = trace (automaton r) (astart r) nn
+    nn09 : (n m : ℕ) → n ≤ n + m
+    nn09 zero m = z≤n
+    nn09 (suc n) m = s≤s (nn09 n m)
     nn04 :  Trace (automaton r) nn (astart r)
     nn04 = tr-accept← (automaton r) nn (astart r) nn03 
+    nntrace = trace (automaton r) (astart r) nn
     nn07 : (n : ℕ) →  length (inputnn0 n i0 i1 []) ≡ n + n 
     nn07 n = subst (λ k → length (inputnn0 n i0 i1 []) ≡ k) (+-comm (n + n) _ ) (nn08 n [] )where
        nn08 : (n : ℕ) → (s : List In2) → length (inputnn0 n i0 i1 s) ≡ n + n + length s
@@ -213,9 +211,6 @@
          suc n + ((n + 1) + length s) ≡⟨ cong (λ k → suc n + (k + length s)) (+-comm n _) ⟩
          suc n + (suc n + length s) ≡⟨ sym (+-assoc (suc n)  _ _) ⟩
          suc n + suc n + length s  ∎  where open ≡-Reasoning
-    nn09 : (n m : ℕ) → n ≤ n + m
-    nn09 zero m = z≤n
-    nn09 (suc n) m = s≤s (nn09 n m)
     nn05 : length nntrace > finite (afin r)
     nn05 = begin
          suc (finite (afin r))  ≤⟨ nn09 _ _ ⟩
@@ -223,44 +218,49 @@
          length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
          {!!} ≤⟨ {!!} ⟩
          length nntrace ∎  where open ≤-Reasoning
-    nn02 : {!!} -- TA (automaton r) {!!} {!!} {!!}
-    nn02 = {!!} where -- make-TA (automaton r) (afin r) (Dup-in-list.dup nn06) _ _ (Dup-in-list.is-dup nn06) ? where
-        nn06 : Dup-in-list ( afin r) nntrace
-        nn06 = dup-in-list>n (afin r) nntrace nn05
-    nn12 : (x y z : List In2)
-        → ¬ y ≡ []
-        → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
-    nn12 x y z p q = {!!} where
-         mono-color : List In2 → Bool
-         mono-color [] = true
-         mono-color (i0 ∷ s) = mono-color0 s where
-              mono-color0 : List In2 → Bool
-              mono-color0 [] = true
-              mono-color0 (i1 ∷ s) = false
-              mono-color0 (i0 ∷ s) = mono-color0 s
-         mono-color (i1 ∷ s) = mono-color1 s where
-              mono-color1 : List In2 → Bool
-              mono-color1 [] = true
-              mono-color1 (i0 ∷ s) = false
-              mono-color1 (i1 ∷ s) = mono-color1 s
-         mono-color (i1 ∷ s) = {!!}
-         i1-i0? : List In2 → Bool
-         i1-i0? [] = false
-         i1-i0? (i1 ∷ []) = false
-         i1-i0? (i0 ∷ []) = false
-         i1-i0? (i1 ∷ i0 ∷ s) = true
-         i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)  
-         nn13 : mono-color y ≡ true → count i0  (x ++ y ++ z) ≡  count i1 (x ++ y ++ z) → 
-             ¬ ( count i0   (x ++ y ++ y ++ z) ≡  count i1  (x ++ y ++ y ++ z) )
-         nn13 = {!!}
-         nn16 :  (s : List In2 ) →  accept  (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
-         nn16 = {!!}
-         nn15 :  (s : List In2 ) → i1-i0? s ≡ true → accept  (automaton r) (astart r) s ≡ false
-         nn15 = {!!}
-         nn14 : mono-color y ≡ false → i1-i0? (x ++ y ++ y ++ z) ≡ true
-         nn14 = {!!}
-         nn17 : accept (automaton r) (astart r) (x ++ y ++ z) ≡ true →  ¬ (accept (automaton r) (astart r)  (x ++ y ++ y ++ z) ≡ true)
-         nn17 p q with mono-color y | inspect mono-color y
-         ... | true | record { eq = eq } = {!!}
-         ... | false | record { eq = eq } = {!!} -- q ( nn15 (x ++ y ++ z) (nn14 eq)) 
-         
+    nn06 : Dup-in-list ( afin r) nntrace
+    nn06 = dup-in-list>n (afin r) nntrace nn05
+    TAnn : TA (automaton r) (astart r) nn
+    TAnn = make-TA (automaton r) (afin r) (astart r) {!!} nn {!!} {!!}
+    count : In2 → List In2 → ℕ
+    count _ [] = 0
+    count i0 (i0 ∷ s) = suc (count i0 s)
+    count i1 (i1 ∷ s) = suc (count i1 s)
+    count x (_ ∷ s) = count x s
+    nn11 : {x : In2} → (s t : List In2) → count x (s ++ t) ≡ count x s + count x t
+    nn11 = {!!}
+    nn10 : (s : List In2) → accept (automaton r) (astart r) s ≡ true → count i0 s ≡ count i1 s
+    nn10 = {!!}
+    i1-i0? : List In2 → Bool
+    i1-i0? [] = false
+    i1-i0? (i1 ∷ []) = false
+    i1-i0? (i0 ∷ []) = false
+    i1-i0? (i1 ∷ i0 ∷ s) = true
+    i1-i0? (_ ∷ s0 ∷ s1) = i1-i0? (s0 ∷ s1)  
+    nn20 : {s s0 s1 : List In2} → accept (automaton r) (astart r) s ≡ true → ¬ ( s ≡ s0 ++ i1 ∷ i0 ∷ s1 )
+    nn20 = {!!}
+    mono-color : List In2 → Bool
+    mono-color [] = true
+    mono-color (i0 ∷ s) = mono-color0 s where
+        mono-color0 : List In2 → Bool
+        mono-color0 [] = true
+        mono-color0 (i1 ∷ s) = false
+        mono-color0 (i0 ∷ s) = mono-color0 s
+    mono-color (i1 ∷ s) = mono-color1 s where
+        mono-color1 : List In2 → Bool
+        mono-color1 [] = true
+        mono-color1 (i0 ∷ s) = false
+        mono-color1 (i1 ∷ s) = mono-color1 s
+    record Is10 (s : List In2) : Set where
+       field
+           s0 s1 : List In2
+           is-10 :  s ≡ s0 ++ i1 ∷ i0 ∷ s1
+    not-mono : { s : List In2 } → ¬ (mono-color s ≡ true)  → Is10 (s ++ s)
+    not-mono = {!!}
+    mono-count : { s : List In2 } → mono-color s ≡ true   → (length s ≡ count i0 s) ∨ ( length s ≡ count i1 s)
+    mono-count = {!!}
+    tann : {x y z : List In2} → ¬ y ≡ []  → accept (automaton r) (astart r) (x ++ y ++ z) ≡ true → ¬ (accept (automaton r) (astart r) (x ++ y ++ y ++ z)  ≡ true )
+    tann {x} {y} {z} ny axyz axyyz with mono-color y
+    ... | true = {!!}
+    ... | false = {!!}
+