Mercurial > hg > Members > kono > Proof > automaton
changeset 309:acb0214ea4d8
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 02 Jan 2022 15:27:17 +0900 |
| parents | 2effd9a23299 |
| children | 271ded718895 |
| files | automaton-in-agda/src/non-regular.agda |
| diffstat | 1 files changed, 6 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- 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 Σ