annotate automaton-in-agda/src/pumping.agda @ 403:c298981108c1

fix for std-lib 2.0
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 11:32:01 +0900
parents 101080136450
children af8f630b7e60
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
385
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 332
diff changeset
1 module pumping where
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Data.Nat
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
4 open import Data.Empty
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.List
278
e89957b99662 dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
6 open import Data.Maybe hiding ( map )
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Relation.Binary.PropositionalEquality hiding ( [_] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import logic
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
9 open import automaton
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
10 open import automaton-ex
278
e89957b99662 dup in finiteSet in long list
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 277
diff changeset
11 open import finiteSetUtil
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open import finiteSet
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 open import Relation.Nullary
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
14 open import regular-language
306
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
15 open import nat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
16
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
274
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
18 open FiniteSet
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
19
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
20 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
21 -- if there is an automaton with n states , which accespt inputnn1, it has a trasition function.
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
22 -- The function is determinted by inputs,
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
23 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
24
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
25 open RegularLanguage
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
26 open Automaton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
27
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 183
diff changeset
28 open _∧_
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29
295
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
30 data Trace { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) : (is : List Σ) → Q → Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
31 tend : {q : Q} → aend fa q ≡ true → Trace fa [] q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
32 tnext : (q : Q) → {i : Σ} { is : List Σ}
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
33 → Trace fa is (δ fa q i) → Trace fa (i ∷ is) q
277
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
34
294
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
35 tr-len : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
36 → (fa : Automaton Q Σ )
295
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
37 → (is : List Σ) → (q : Q) → Trace fa is q → suc (length is) ≡ length (trace fa q is )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
38 tr-len {Q} {Σ} fa .[] q (tend x) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
39 tr-len {Q} {Σ} fa (i ∷ is) q (tnext .q t) = cong suc (tr-len {Q} {Σ} fa is (δ fa q i) t)
294
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
40
277
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
41 tr-accept→ : { Q : Set } { Σ : Set }
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
42 → (fa : Automaton Q Σ )
295
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
43 → (is : List Σ) → (q : Q) → Trace fa is q → accept fa q is ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
44 tr-accept→ {Q} {Σ} fa [] q (tend x) = x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
45 tr-accept→ {Q} {Σ} fa (i ∷ is) q (tnext _ tr) = tr-accept→ {Q} {Σ} fa is (δ fa q i) tr
277
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
46
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
47 tr-accept← : { Q : Set } { Σ : Set }
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
48 → (fa : Automaton Q Σ )
295
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
49 → (is : List Σ) → (q : Q) → accept fa q is ≡ true → Trace fa is q
277
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
50 tr-accept← {Q} {Σ} fa [] q ac = tend ac
295
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
51 tr-accept← {Q} {Σ} fa (x ∷ []) q ac = tnext _ (tend ac )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
52 tr-accept← {Q} {Σ} fa (x ∷ x1 ∷ is) q ac = tnext _ (tr-accept← fa (x1 ∷ is) (δ fa q x) ac)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
53
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
54 tr→qs : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
55 → (fa : Automaton Q Σ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
56 → (is : List Σ) → (q : Q) → Trace fa is q → List Q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
57 tr→qs fa [] q (tend x) = []
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
58 tr→qs fa (i ∷ is) q (tnext q tr) = q ∷ tr→qs fa is (δ fa q i) tr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
59
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
60 tr→qs=is : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
61 → (fa : Automaton Q Σ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
62 → (is : List Σ) → (q : Q) → (tr : Trace fa is q ) → length is ≡ length (tr→qs fa is q tr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
63 tr→qs=is fa .[] q (tend x) = refl
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
64 tr→qs=is fa (i ∷ is) q (tnext .q tr) = cong suc (tr→qs=is fa is (δ fa q i) tr)
277
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
65
294
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
66 open Data.Maybe
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
67
403
c298981108c1 fix for std-lib 2.0
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 385
diff changeset
68 -- open import Relation.Binary.HeterogeneousEquality as HE using (_≅_ )
306
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
69 open import Relation.Binary.Definitions
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
70 open import Data.Unit using (⊤ ; tt)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
71 open import Data.Nat.Properties
294
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
72
309
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
73 data QDSEQ { Q : Set } { Σ : Set } { fa : Automaton Q Σ} ( finq : FiniteSet Q) (qd : Q) (z1 : List Σ) :
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
74 {q : Q} {y2 : List Σ} → Trace fa (y2 ++ z1) q → Set where
311
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
75 qd-nil : (q : Q) → (tr : Trace fa z1 q) → equal? finq qd q ≡ true → QDSEQ finq qd z1 tr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
76 qd-next : {i : Σ} (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) (δ fa q i)) → equal? finq qd q ≡ false
309
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
77 → QDSEQ finq qd z1 tr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
78 → QDSEQ finq qd z1 (tnext q tr)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 308
diff changeset
79
302
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
80 record TA1 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
81 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
82 y z : List Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
83 yz=is : y ++ z ≡ is
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
84 trace-z : Trace fa z qd
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
85 trace-yz : Trace fa (y ++ z) q
310
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
86 q=qd : QDSEQ finq qd z trace-yz
316
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
87
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
88 --
317
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 316
diff changeset
89 -- using accept ≡ true may simplify the pumping-lemma
316
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
90 -- QDSEQ is too complex, should we generate (lengty y ≡ 0 → equal ) ∧ ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
91 --
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
92 -- like this ...
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
93 -- record TA2 { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) ( q qd : Q ) (is : List Σ) : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
94 -- field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
95 -- y z : List Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
96 -- yz=is : y ++ z ≡ is
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
97 -- trace-z : accpet fa z qd ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
98 -- trace-yz : accept fa (y ++ z) q ≡ true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
99 -- q=qd : last (tr→qs fa q trace-yz) ≡ just qd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
100 -- ¬q=qd : non-last (tr→qs fa q trace-yz) ≡ just qd
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
101
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
102 record TA { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) ( q : Q ) (is : List Σ) : Set where
279
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 278
diff changeset
103 field
296
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
104 x y z : List Σ
298
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 297
diff changeset
105 xyz=is : x ++ y ++ z ≡ is
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
106 trace-xyz : Trace fa (x ++ y ++ z) q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
107 trace-xyyz : Trace fa (x ++ y ++ y ++ z) q
304
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 303
diff changeset
108 non-nil-y : ¬ (y ≡ [])
296
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 295
diff changeset
109
317
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 316
diff changeset
110 pumping-lemma : { Q : Set } { Σ : Set } (fa : Automaton Q Σ ) (finq : FiniteSet Q) (q qd : Q) (is : List Σ)
295
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
111 → (tr : Trace fa is q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 294
diff changeset
112 → dup-in-list finq qd (tr→qs fa is q tr) ≡ true
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
113 → TA fa q is
317
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 316
diff changeset
114 pumping-lemma {Q} {Σ} fa finq q qd is tr dup = tra-phase1 q is tr dup where
294
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 291
diff changeset
115 open TA
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
116 tra-phase2 : (q : Q) → (is : List Σ) → (tr : Trace fa is q )
302
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
117 → phase2 finq qd (tr→qs fa is q tr) ≡ true → TA1 fa finq q qd is
297
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
118 tra-phase2 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect ( equal? finq qd) q
311
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
119 ... | true | record { eq = eq } = record { y = [] ; z = i ∷ is ; yz=is = refl ; q=qd = qd-nil q (tnext q tr) eq
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
120 ; trace-z = subst (λ k → Trace fa (i ∷ is) k ) (sym (equal→refl finq eq)) (tnext q tr) ; trace-yz = tnext q tr }
310
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
121 ... | false | record { eq = ne } = record { y = i ∷ TA1.y ta ; z = TA1.z ta ; yz=is = cong (i ∷_ ) (TA1.yz=is ta )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
122 ; q=qd = tra-08
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
123 ; trace-z = TA1.trace-z ta ; trace-yz = tnext q ( TA1.trace-yz ta ) } where
302
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
124 ta : TA1 fa finq (δ fa q i) qd is
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
125 ta = tra-phase2 (δ fa q i) is tr p
310
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
126 tra-07 : Trace fa (TA1.y ta ++ TA1.z ta) (δ fa q i)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
127 tra-07 = subst (λ k → Trace fa k (δ fa q i)) (sym (TA1.yz=is ta)) tr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 309
diff changeset
128 tra-08 : QDSEQ finq qd (TA1.z ta) (tnext q (TA1.trace-yz ta))
311
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
129 tra-08 = qd-next (TA1.y ta) q (TA1.trace-yz (tra-phase2 (δ fa q i) is tr p)) ne (TA1.q=qd ta)
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
130 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
297
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 296
diff changeset
131 tra-phase1 q (i ∷ is) (tnext q tr) p with equal? finq qd q | inspect (equal? finq qd) q
315
25ae77240238 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 314
diff changeset
132 ... | true | record { eq = eq } = record { x = [] ; y = i ∷ TA1.y ta ; z = TA1.z ta ; xyz=is = cong (i ∷_ ) (TA1.yz=is ta)
304
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 303
diff changeset
133 ; non-nil-y = λ ()
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
134 ; trace-xyz = tnext q (TA1.trace-yz ta)
314
a69308ed107a tra-phase1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
135 ; trace-xyyz = tnext q tra-05 } where
302
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 301
diff changeset
136 ta : TA1 fa finq (δ fa q i ) qd is
300
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 299
diff changeset
137 ta = tra-phase2 (δ fa q i ) is tr p
308
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
138 y1 = TA1.y ta
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
139 z1 = TA1.z ta
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
140 tryz0 : Trace fa (y1 ++ z1) (δ fa qd i)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
141 tryz0 = subst₂ (λ j k → Trace fa k (δ fa j i) ) (sym (equal→refl finq eq)) (sym (TA1.yz=is ta)) tr
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
142 tryz : Trace fa (i ∷ y1 ++ z1) qd
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
143 tryz = tnext qd tryz0
316
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 315
diff changeset
144 -- create Trace (y ++ y ++ z)
308
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
145 tra-04 : (y2 : List Σ) → (q : Q) → (tr : Trace fa (y2 ++ z1) q)
315
25ae77240238 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 314
diff changeset
146 → QDSEQ finq qd z1 {q} {y2} tr
306
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 305
diff changeset
147 → Trace fa (y2 ++ (i ∷ y1) ++ z1) q
312
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
148 tra-04 [] q tr (qd-nil q _ x₁) with equal? finq qd q | inspect (equal? finq qd) q
308
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 307
diff changeset
149 ... | true | record { eq = eq } = subst (λ k → Trace fa (i ∷ y1 ++ z1) k) (equal→refl finq eq) tryz
312
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
150 ... | false | record { eq = ne } = ⊥-elim ( ¬-bool refl x₁ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 311
diff changeset
151 tra-04 (y0 ∷ y2) q (tnext q tr) (qd-next _ _ _ x₁ qdseq) with equal? finq qd q | inspect (equal? finq qd) q
315
25ae77240238 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 314
diff changeset
152 ... | true | record { eq = eq } = ⊥-elim ( ¬-bool x₁ refl )
311
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 310
diff changeset
153 ... | false | record { eq = ne } = tnext q (tra-04 y2 (δ fa q y0) tr qdseq )
314
a69308ed107a tra-phase1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
154 tra-05 : Trace fa (TA1.y ta ++ (i ∷ TA1.y ta) ++ TA1.z ta) (δ fa q i)
a69308ed107a tra-phase1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
155 tra-05 with equal→refl finq eq
a69308ed107a tra-phase1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 313
diff changeset
156 ... | refl = tra-04 y1 (δ fa qd i) (TA1.trace-yz ta) (TA1.q=qd ta)
315
25ae77240238 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 314
diff changeset
157 ... | false | _ = record { x = i ∷ x ta ; y = y ta ; z = z ta ; xyz=is = cong (i ∷_ ) (xyz=is ta)
304
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 303
diff changeset
158 ; non-nil-y = non-nil-y ta
299
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
159 ; trace-xyz = tnext q (trace-xyz ta ) ; trace-xyyz = tnext q (trace-xyyz ta )} where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
160 ta : TA fa (δ fa q i ) is
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 298
diff changeset
161 ta = tra-phase1 (δ fa q i ) is tr p
277
42563cc6afdf non-regular
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 274
diff changeset
162