# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1640511408 -32400
# Node ID 797fdfe65c9306077c132620bf4db3accd115f31
# Parent  e89957b99662fc6464a27844e84a059bb5d4ed2d
...

diff -r e89957b99662 -r 797fdfe65c93 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Sun Dec 26 12:38:37 2021 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Dec 26 18:36:48 2021 +0900
@@ -69,28 +69,42 @@
 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext (tend ac )
 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext (tr-accept← fa (x1 ∷ is)  (δ fa q x)  ac) 
 
+open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ ) 
 
-tr-append-is : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
-     →  memberQ finq q qs ≡ true 
-     →  Trace fa is (q ∷ qs) → List Σ ∧ List Q
-tr-append-is {Q} {Σ} fa finq q [] [] () (tend x)
-tr-append-is {Q} {Σ} fa finq q (x ∷ is) [] () tr
-tr-append-is {Q} {Σ} fa finq q (x ∷ is) (q0 ∷ qs) mb tr with equal? finq q q0
-... | true = ⟪ x ∷ [] , q0 ∷ [] ⟫
-tr-append-is {Q} {Σ} fa finq q (x ∷ is) (.(δ fa q x) ∷ qs) mb (tnext tr) | false = tr3 (δ fa q x ∷ qs) tr2 is tr  where
-     tr2 : memberQ finq q (δ fa q x ∷ qs) ≡ true
-     tr2 = {!!}
-     tr3 : (qs : List Q) → memberQ finq q qs ≡ true → (is :  List Σ) → Trace fa is qs → List Σ ∧ List Q
-     tr3 (x ∷ []) mb [] (tend x₁) = {!!}
-     tr3 (q0 ∷ qs) mb (x₁ ∷ is) (tnext tr) with equal? finq q q0
-     ... | true = ⟪ x ∷ [] , {!!} ⟫
-     ... | false = ⟪ x ∷ proj1 (tr3 qs mb is tr) , {!!} ⟫
+record TA { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) {is : List Σ} { qs : List Q } (tr : Trace fa is qs) : Set where
+    field
+       x y z : List Σ
+       qx qy qz : List Q
+       trace0 : Trace fa (x ++ y ++ z) (qx ++ qy ++ qz) 
+       trace1 : Trace fa (x ++ y ++ y ++ z) (qx ++ qy ++ qy ++ qz) 
+       trace-eq : trace0 ≅ tr
 
 tr-append : { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q) (q : Q) (is : List Σ) ( qs : List Q )
-     → (mb :  memberQ finq q qs ≡ true )
-     → (tr : Trace fa is ( q ∷ qs ))
-     → Trace fa (proj1 (tr-append-is fa finq q is qs mb tr) ++ is) (proj2 (tr-append-is fa finq q is qs mb tr) ++ (q ∷ qs))
-tr-append = {!!}
+     →  dup-in-list finq q qs ≡ true
+     →  (tr : Trace fa is qs ) → TA fa tr
+tr-append {Q} {Σ} fa finq q is qs dup tr = tra-phase1 qs is tr dup where
+   tra-phase3 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → {!!}
+        → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true → {!!}
+        → Trace fa (iy ++ is) (qy ++ qs)
+   tra-phase3 = {!!}
+   tra-phase2 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase2 finq q qs ≡ true
+        → (qy : List Q) → (iy : List Σ)  → (ty : Trace fa iy qy ) → phase2 finq q qy ≡ true
+        → TA fa tr
+   tra-phase2 (q0 ∷ []) is (tend x₁) p qy iy ty py = {!!}
+   tra-phase2 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p qy iy ty py with equal? finq q q0
+   ... | true = {!!}
+   ... | false = {!!} where
+       tr1 : TA fa tr
+       tr1 = tra-phase2 (q₁ ∷ qs) is tr p qy iy ty py
+   tra-phase1 : (qs : List Q) → (is : List Σ)  → (tr : Trace fa is qs ) → phase1 finq q qs ≡ true  → TA fa tr
+   tra-phase1 (q0 ∷ []) is (tend x₁) p = {!!}
+   tra-phase1 (q0 ∷ (q₁ ∷ qs)) (x ∷ is) (tnext tr) p with equal? finq q q0
+   ... | true = {!!} where
+       tr2 : TA fa tr
+       tr2 = tra-phase2 (q₁ ∷ qs) is tr p (q₁ ∷ qs) is tr p
+   ... | false = {!!} where
+       tr1 : TA fa tr
+       tr1 = tra-phase1 (q₁ ∷ qs) is tr p
 
 lemmaNN : (r : RegularLanguage In2 ) → ¬ ( (s : List In2)  → isRegular inputnn1  s r ) 
 lemmaNN r Rg = {!!}