# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1641137401 -32400
# Node ID a69308ed107a972f7a01a8ddbbf537df657d5f5d
# Parent  ae33e1504f2b08631a370baff7df00e7a18c579c
tra-phase1 done

diff -r ae33e1504f2b -r a69308ed107a automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Mon Jan 03 00:22:46 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Mon Jan 03 00:30:01 2022 +0900
@@ -164,20 +164,15 @@
    ... | 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 = tnext q (subst (λ k → Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa k i)  )
-                (equal→refl finq eq) (tra-04 (TA1.y ta) (δ fa qd i) tryz0 (qdseq1 (TA1.q=qd ta)))) } where
+           ; trace-xyyz = tnext q tra-05 } where
         ta : TA1 fa finq (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
         y1 = TA1.y ta
         z1 = TA1.z ta
         tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
         tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
-        tryz1 : Trace fa (y1 ++ z1) (δ fa q i)
-        tryz1 = TA1.trace-yz ta
         tryz : Trace fa (i ∷ y1 ++ z1) qd
         tryz = tnext qd tryz0
-        qdseq1 : QDSEQ finq qd z1 {δ fa q i} {y1} (TA1.trace-yz ta) → QDSEQ finq qd z1 {δ fa qd i} {y1} tryz0
-        qdseq1 drs = {!!}
         tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
                →  QDSEQ finq qd z1 {q} {y2} tr -- should be y ++ z1
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
@@ -187,6 +182,9 @@
         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
         ... | 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