# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640948574 -32400
# Node ID 67d8e42b7782f554129cad8b9903cb1738354163
# Parent  841f4064e51585e7309efe274ac2b4957e2efcb7
...

diff -r 841f4064e515 -r 67d8e42b7782 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Fri Dec 31 17:27:58 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Fri Dec 31 20:02:54 2021 +0900
@@ -105,11 +105,11 @@
 
 open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
+record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q qd : Q ) (is : List Σ)  : Set where
     field
        y z : List Σ
        yz=is : y ++ z ≡ is 
-       trace-z    : Trace fa z  q
+       trace-z    : Trace fa z  qd
        trace-yz   : Trace fa (y ++ z)  q
 
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
@@ -127,34 +127,36 @@
      → TA fa q is
 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 q is
+   tra-phase2 : (q : Q)  → (is : List Σ)  → (tr : Trace fa is  q )
+       → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa q qd is
    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 } = {!!} 
+   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl
+        ; trace-z  = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
+   ... | false | record { eq = eq } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
+       ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
+            ta : TA1 fa (δ fa q i) qd is
+            ta = tra-phase2 (δ fa q i) is tr p 
    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)
-           ; trace-xyz  = {!!}
-           ; trace-xyyz = {!!} } where
---  : phase2 finq qd (tr→qs fa (y ta ++ z ta) qd (trace-yz ta a<sa))
---    ≡ true
---  : phase1 finq qd (tr→qs fa (y ta ++ z ta) qd (trace-yz ta a<sa))
---    ≡ false
-        ta : TA1 fa (δ fa q i ) is
-        ta = tra-phase2 (δ fa q i ) is tr p
-        tra-02 : (y1 : List Σ) → (q : Q) → (tr : Trace fa (y1 ++ TA1.z ta) q)
-            → phase2 finq qd (tr→qs fa (y1 ++ TA1.z ta) q tr) ≡ true
-            → phase1 finq qd (tr→qs fa (y1 ++ TA1.z ta) q tr) ≡ false
-            → Trace fa (y1 ++ TA1.y ta ++ TA1.z ta) q
-        tra-02 [] q tr p np with equal? finq qd q | inspect ( equal? finq qd) q
-        ... | true  | record { eq = eq } = subst (λ k →  Trace fa (TA1.y ta ++ TA1.z ta) k ) (equal→refl finq eq) (TA1.trace-yz ta )
+           ; trace-xyz  = tnext q (TA1.trace-yz ta)
+           ; trace-xyyz = tnext q (tra-02 ? ? ? (TA1.trace-yz ta) ? ? ) } where
+              -- tra-02 (i ∷  TA1.y ta) q (sym (equal→refl finq eq)) (tnext q (TA1.trace-yz ta)) {!!} {!!} } where
+        ta : TA1 fa (δ fa q i ) qd is
+        ta = tra-phase2 (δ fa q i ) is tr p 
+        tra-02 : (y1 : List Σ) → (q0 : Q) → q ≡ qd  → (tr : Trace fa (y1 ++ TA1.z ta) (δ fa q i))
+            → phase2 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ true
+            → phase1 finq qd (tr→qs fa (y1 ++ TA1.z ta) q0 tr) ≡ false
+            → Trace fa (y1 ++ i ∷ TA1.y ta ++ TA1.z ta) (δ fa q0 i)
+        tra-02 [] q0 q=qd tr p np with equal? finq qd q0 | inspect ( equal? finq qd) q0
+        ... | true  | record { eq = eq } = subst (λ k →  Trace fa (i ∷ TA1.y ta ++ TA1.z ta) k  ) {!!} (tnext q (TA1.trace-yz ta)  ) where
+            tra-03 : q ≡ q0 
+            tra-03 = trans q=qd ((equal→refl finq eq) )
         ... | false | record { eq = ne } = {!!}
-        tra-02 (y1 ∷ ys) q (tnext q tr) p np with equal? finq qd q | inspect ( equal? finq qd) q
+        tra-02 (y1 ∷ ys) q0 q=qd (tnext q tr) p np with equal? finq qd q | inspect ( equal? finq qd) q
         ... | true  | record { eq = eq } = {!!}
-        ... | false | record { eq = ne } = tnext q (tra-02 ys (δ fa q y1) tr p np )
-        tra-01 : (y1 : List Σ) → Trace fa (y1 ++ TA1.z ta) qd → Trace fa (y1 ++ TA1.y ta ++ TA1.z ta) qd
-        tra-01 = {!!}
+        ... | false | record { eq = ne } = {!!} -- tnext q (tra-02 ys (δ fa q y1) q=qd tr p np )
    ... | 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)
             ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
         ta : TA fa (δ fa q i ) is