# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1641117096 -32400
# Node ID 271ded718895d960216f9c2dcf1688ee51c74d52
# Parent  acb0214ea4d86680ca6001d44fb9923b5f5f325e
...

diff -r acb0214ea4d8 -r 271ded718895 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Sun Jan 02 15:27:17 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Jan 02 18:51:36 2022 +0900
@@ -116,7 +116,8 @@
 
 data QDSEQ { Q : Set } { Σ : Set  } { fa : Automaton  Q  Σ} ( finq : FiniteSet Q) (qd : Q) (z1 :  List Σ) :
        {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
-   qd-next : (i : Σ) (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ is0-bool (length y2)
+   qd-nil : (i : Σ)  → (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
+   qd-next : (i : Σ) (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false
        → QDSEQ finq qd z1 tr 
        → QDSEQ finq qd z1 (tnext q tr)
 
@@ -126,7 +127,8 @@
        yz=is : y ++ z ≡ is 
        trace-z    : Trace fa z  qd
        trace-yz   : Trace fa (y ++ z)  q
-       q=qd : equal? finq qd q ≡ is0-bool (length y)
+       q=qd : QDSEQ finq qd z trace-yz
+       -- q=qd : equal? finq qd q ≡ is0-bool (length y)
 
 record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ )   ( q : Q ) (is : List Σ)  : Set where
     field
@@ -145,19 +147,25 @@
    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
    tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
-   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = eq
+   ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil i q (tnext q tr) eq
         ; 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 ) ; q=qd = eq
+   ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
+       ; q=qd = tra-08
        ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
             ta : TA1 fa finq (δ fa q i) qd is
             ta = tra-phase2 (δ fa q i) is tr p 
+            tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
+            tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
+            tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
+            tra-08 = qd-next i (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)
            ; non-nil-y = λ ()
            ; trace-xyz  = tnext q (TA1.trace-yz ta)
-           ; trace-xyyz = tra-04 (i ∷ TA1.y ta) q (tnext q (subst (λ k → Trace fa (y1 ++ z1) (δ fa k i) ) (equal→refl finq eq) tryz0)) } where 
+           ; trace-xyyz = tra-04 (i ∷ TA1.y ta) q (tnext q (subst (λ k → Trace fa (y1 ++ z1) (δ fa k i) ) (equal→refl finq eq) tryz0))
+              (λ y2 q tr → tra-051 y2 q tr {!!} ) } where 
         ta : TA1 fa finq (δ fa q i ) qd is
         ta = tra-phase2 (δ fa q i ) is tr p 
         y1 = TA1.y ta
@@ -166,18 +174,20 @@
         tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
         tryz : Trace fa (i ∷ y1 ++ z1) qd
         tryz = tnext qd tryz0
-        tra-06 : equal? finq qd (δ fa q i) ≡ is0-bool (length y1)
+        tra-06 : QDSEQ finq qd (TA1.z ta) (TA1.trace-yz ta)
         tra-06 = TA1.q=qd ta 
-        tra-05 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → equal? finq qd q ≡ is0-bool (length y2)
-        tra-05 y2 q tr = {!!}
+        tra-051 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → QDSEQ finq qd z1 tr → equal? finq qd q ≡ is0-bool (length y2)
+        tra-051 .[] q tr (qd-nil i .q .tr x₁) = x₁
+        tra-051 .(i ∷ y2) q .(tnext q tr) (qd-next i y2 .q tr x₁ qdseq) = x₁
         tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
+               → (tra-05 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q) → equal? finq qd q ≡ is0-bool (length y2))
                → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
-        tra-04 [] q tr with equal? finq qd q | inspect (equal? finq qd) q
+        tra-04 [] q tr tra-05 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  ne (tra-05 [] q tr) ) 
-        tra-04 (y0 ∷ y2) q (tnext q tr) with equal? finq qd q | inspect (equal? finq qd) q
+        tra-04 (y0 ∷ y2) q (tnext q tr) tra-05 with equal? finq qd q | inspect (equal? finq qd) q
         ... | true | record { eq = eq } = ⊥-elim ( ¬-bool (tra-05 (y0 ∷ y2) q (tnext q tr)) eq ) where -- y2 + z1 contains two qd
-        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr ) 
+        ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr tra-05 ) 
    ... | 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