# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1641138906 -32400
# Node ID 25ae772402385b2a5cfcf6740b3c0ec7afdc09be
# Parent  a69308ed107a972f7a01a8ddbbf537df657d5f5d
clean up

diff -r a69308ed107a -r 25ae77240238 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Mon Jan 03 00:30:01 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Mon Jan 03 00:55:06 2022 +0900
@@ -138,11 +138,11 @@
        trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
        non-nil-y : ¬ (y ≡ [])
 
-make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (fins : FiniteSet Σ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
+make-TA : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ) 
      → (tr : Trace fa is q )
      → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
      → TA fa q is
-make-TA {Q} {Σ} fa fins finq q qd is tr dup = tra-phase1 q is tr dup where
+make-TA {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
    open TA
    tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q )
        → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
@@ -160,8 +160,7 @@
             tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p))  ne (TA1.q=qd ta)
    tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q is
    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)
+   ... | true | record { eq = eq } = 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 = tnext q tra-05 } where
@@ -174,23 +173,18 @@
         tryz : Trace fa (i ∷ y1 ++ z1) qd
         tryz = tnext qd tryz0
         tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
-               →  QDSEQ finq qd z1 {q} {y2} tr -- should be y ++ z1
+               →  QDSEQ finq qd z1 {q} {y2} tr 
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
         tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
         ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
         ... | false | record { eq = ne } = ⊥-elim ( ¬-bool  refl x₁ ) 
         tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _  _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
-        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) -- y2 + z1 contains two qd
+        ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl ) 
         ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq ) 
         tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
         tra-05 with equal→refl finq eq
         ... | refl = tra-04 y1  (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
-   ... | 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) 
+   ... | 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
@@ -216,7 +210,7 @@
     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
+    nntrace = tr→qs (automaton r) nn (astart r) nn04
     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
@@ -236,10 +230,10 @@
          length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
          {!!} ≤⟨ {!!} ⟩
          length nntrace ∎  where open ≤-Reasoning
-    nn06 : Dup-in-list ( afin r) nntrace
+    nn06 : Dup-in-list ( afin r) (tr→qs (automaton r) nn (astart r) nn04)
     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 {!!} {!!}
+    TAnn = make-TA (automaton r) (afin r) (astart r) (Dup-in-list.dup nn06) nn nn04 (Dup-in-list.is-dup nn06)
     count : In2 → List In2 → ℕ
     count _ [] = 0
     count i0 (i0 ∷ s) = suc (count i0 s)