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

diff -r 2effd9a23299 -r acb0214ea4d8 automaton-in-agda/src/non-regular.agda
--- a/automaton-in-agda/src/non-regular.agda	Sun Jan 02 06:52:35 2022 +0900
+++ b/automaton-in-agda/src/non-regular.agda	Sun Jan 02 15:27:17 2022 +0900
@@ -114,6 +114,12 @@
 is0-bool zero = true
 is0-bool (suc i) = false
 
+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)
+       → QDSEQ finq qd z1 tr 
+       → QDSEQ finq qd z1 (tnext q tr)
+
 record TA1 { Q : Set } { Σ : Set  } (fa : Automaton Q  Σ ) (finq : FiniteSet Q)  ( q qd : Q ) (is : List Σ)  : Set where
     field
        y z : List Σ