# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640932947 -32400
# Node ID afc7db9b917d15a7b2e3aed433ea049eedd2cb94
# Parent  2f113cac060bc6abd87455ee9fab6aab289eb56b
...

diff -r 2f113cac060b -r afc7db9b917d automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Fri Dec 31 14:36:44 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Dec 31 15:42:27 2021 +0900
@@ -122,17 +122,25 @@
 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 1 q qd
-   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q
-   ... | true = {!!} 
-   ... | false = {!!}
+   tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
+   ... | true | record { eq = eq } = {!!} 
+   ... | false | record { eq = eq } = {!!} 
    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 : {!!}
+   tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
+   ... | true | record { eq = eq } = 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 ) (equal→refl finq eq) (trace-yz TA0 a<sa)
+           ; trace-xyyz = λ _ → subst (λ k → Trace fa (y TA0 ++ y TA0 ++ z TA0) k ) (equal→refl finq eq) (tra-01 (y TA0) (trace-yz TA0 a<sa)) } where
+        TA0 : TA fa 1 (δ fa q i ) qd 
         TA0 = tra-phase2 (δ fa q i ) is tr p
-   ... | false = record { x = i ∷ x TA0 ; y = y TA0 ; z = z TA0 ; trace-z = λ () ; trace-yz = λ ()
+        tra-02 : (y1 : List Σ) → (q : Q) → (tr : Trace fa (y1 ++ z TA0) q)
+            → phase2 finq qd (tr→qs fa (y1 ++ z TA0) q tr) ≡ true  → Trace fa (y1 ++ y TA0 ++ z TA0) q
+        tra-02 [] q tr p with equal? finq qd q | inspect ( equal? finq qd) q
+        ... | true | record { eq = eq } = subst (λ k →  Trace fa (y TA0 ++ z TA0) k ) (equal→refl finq eq) (trace-yz TA0 a<sa )
+        ... | false | record { eq = eq } = {!!}
+        tra-02 (y1 ∷ ys) q (tnext q tr) p = tnext q (tra-02 ys (δ fa q y1) tr {!!} )
+        tra-01 : (y1 : List Σ) → Trace fa (y1 ++ z TA0) qd → Trace fa (y1 ++ y TA0 ++ z TA0) qd
+        tra-01 = {!!}
+   ... | 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