--- a/automaton-in-agda/src/non-regular.agda	Thu Dec 30 17:42:44 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Dec 31 14:36:44 2021 +0900
@@ -105,41 +105,36 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )  ( q : Q ) (phase yeq : Bool)  : Set where
+record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (phase : ℕ)  ( q qd : Q )  : Set where
     field
-       x y y1 z : List Σ
-       px : phase ≡ true → x ≡ []
-       py : yeq ≡ true → y ≡ y1
-       trace0 : Trace fa (x ++ y ++ z)  q
-       trace1 : Trace fa (x ++ y ++ y1 ++ z) q
+       x y z : List Σ
+       trace-z    : phase > 1 → Trace fa z  qd
+       trace-yz   : phase > 0 → Trace fa (y ++ z)  qd
+       trace-xyz  : phase ≡ 0 → Trace fa (x ++ y ++ z)  q
+       trace-xyyz : phase ≡ 0 → Trace fa (x ++ y ++ y ++ z) q
+
+open import nat
 
 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 false true
+     → TA fa 0 q qd 
 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  → TA fa q true false
+   tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase2 finq qd (tr→qs fa is q tr) ≡ true  → TA fa 1 q qd
    tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q
-   ... | true = {!!} -- record { px = λ _ → refl ; x = [] ; y = i ∷ y TA0 ; z = z TA0 ; trace0 = tnext q (trace0 TA0 ) ; trace1 = tnext q (trace1 TA0) } 
-   ... | false = record { px = λ _ → refl ; x = [] ; y = i ∷ y TA0 ; y1 = y1 TA0 ; z = z TA0 ; py = λ ()
-      ; trace0 = tnext q (subst (λ k → Trace fa k (δ fa q i) ) (tr-01 (px TA0 refl ) ) (trace0 TA0))
-      ; trace1 = tnext q (subst (λ k → Trace fa k (δ fa q i) ) (tr-02 (px TA0 refl )) (trace1 TA0))} where
-        TA0 : TA fa (δ fa q i ) true false
+   ... | true = {!!} 
+   ... | false = {!!}
+   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa 0 q qd 
+   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q
+   ... | true = record { x = [] ; y = y TA0 ;  z = z TA0 ; trace-z = λ () ; trace-yz = λ _ → trace-yz TA0 a<sa 
+           ; trace-xyz  = λ _ → subst (λ k → Trace fa (y TA0 ++ z TA0) k ) {!!}  (trace-yz TA0 a<sa)
+           ; trace-xyyz = λ _ → {!!}} where
+        TA0 : {!!}
         TA0 = tra-phase2 (δ fa q i ) is tr p
-        tr-01 : {x1 : List Σ} → x1 ≡ [] → x1 ++ y TA0 ++ z TA0 ≡ y TA0 ++ z TA0
-        tr-01 refl = refl 
-        tr-02 : {x1 : List Σ} → x1 ≡ [] → x1 ++ y TA0  ++ (y1 TA0) ++ z TA0 ≡ y TA0  ++ (y1 TA0) ++ z TA0
-        tr-02 refl = refl 
-   tra-phase1 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q ) → phase1 finq qd (tr→qs fa is q tr) ≡ true  → TA fa q false true
-   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q
-   ... | true = record { px = λ () ; x = i ∷ x TA0 ; y = y TA0 ; y1 = y TA0 ; z = z TA0 ; py = λ _ → refl
-           ; trace0 = tnext q (trace0 TA0 ) ; trace1 = tnext q {!!} } where
-        TA0 : TA fa (δ fa q i ) true false
-        TA0 = tra-phase2 (δ fa q i ) is tr p
-   ... | false = record { px = λ () ; x = i ∷ x TA0 ; y = y TA0 ; y1 = y TA0 ; z = z TA0 ; py = λ _ → refl ; trace0 = tnext q (trace0 TA0 )
-           ; trace1 = tnext q {!!} } where
-        TA0 : TA fa (δ fa q i ) false true
+   ... | false = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ ()
+            ; trace-xyz = λ _ → tnext q (trace-xyz TA0 refl ) ; trace-xyyz = λ _ → tnext q (trace-xyyz TA0 refl )} where
+        TA0 : TA fa 0 (δ fa q i ) qd 
         TA0 = tra-phase1 (δ fa q i ) is tr p
 
 open RegularLanguage
@@ -191,7 +186,7 @@
          length (inputnn0 n i0 i1 []) ≤⟨ refl-≤s  ⟩
          {!!} ≤⟨ {!!} ⟩
          length nntrace ∎  where open ≤-Reasoning
-    nn02 : TA (automaton r) {!!} {!!} {!!}
+    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