|
65
|
1 module regular-language where
|
|
|
2
|
|
|
3 open import Level renaming ( suc to Suc ; zero to Zero )
|
|
|
4 open import Data.List
|
|
|
5 open import Data.Nat hiding ( _≟_ )
|
|
70
|
6 open import Data.Fin hiding ( _+_ )
|
|
72
|
7 open import Data.Empty
|
|
101
|
8 open import Data.Unit
|
|
65
|
9 open import Data.Product
|
|
|
10 -- open import Data.Maybe
|
|
|
11 open import Relation.Nullary
|
|
|
12 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
|
13 open import logic
|
|
70
|
14 open import nat
|
|
65
|
15 open import automaton
|
|
|
16 open import finiteSet
|
|
|
17
|
|
|
18 language : { Σ : Set } → Set
|
|
|
19 language {Σ} = List Σ → Bool
|
|
|
20
|
|
|
21 language-L : { Σ : Set } → Set
|
|
|
22 language-L {Σ} = List (List Σ)
|
|
|
23
|
|
|
24 open Automaton
|
|
|
25
|
|
|
26 record RegularLanguage ( Σ : Set ) : Set (Suc Zero) where
|
|
|
27 field
|
|
|
28 states : Set
|
|
|
29 astart : states
|
|
70
|
30 aℕ : ℕ
|
|
|
31 afin : FiniteSet states {aℕ}
|
|
65
|
32 automaton : Automaton states Σ
|
|
|
33 contain : List Σ → Bool
|
|
|
34 contain x = accept automaton astart x
|
|
|
35
|
|
|
36 Union : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
37 Union {Σ} A B x = (A x ) \/ (B x)
|
|
|
38
|
|
|
39 split : {Σ : Set} → (List Σ → Bool)
|
|
|
40 → ( List Σ → Bool) → List Σ → Bool
|
|
|
41 split x y [] = x [] /\ y []
|
|
|
42 split x y (h ∷ t) = (x [] /\ y (h ∷ t)) \/
|
|
|
43 split (λ t1 → x ( h ∷ t1 )) (λ t2 → y t2 ) t
|
|
|
44
|
|
|
45 Concat : {Σ : Set} → ( A B : language {Σ} ) → language {Σ}
|
|
|
46 Concat {Σ} A B = split A B
|
|
|
47
|
|
|
48 {-# TERMINATING #-}
|
|
|
49 Star : {Σ : Set} → ( A : language {Σ} ) → language {Σ}
|
|
|
50 Star {Σ} A = split A ( Star {Σ} A )
|
|
|
51
|
|
87
|
52 test-AB→split : {Σ : Set} → {A B : List In2 → Bool} → split A B ( i0 ∷ i1 ∷ i0 ∷ [] ) ≡ (
|
|
69
|
53 ( A [] /\ B ( i0 ∷ i1 ∷ i0 ∷ [] ) ) \/
|
|
|
54 ( A ( i0 ∷ [] ) /\ B ( i1 ∷ i0 ∷ [] ) ) \/
|
|
|
55 ( A ( i0 ∷ i1 ∷ [] ) /\ B ( i0 ∷ [] ) ) \/
|
|
|
56 ( A ( i0 ∷ i1 ∷ i0 ∷ [] ) /\ B [] )
|
|
|
57 )
|
|
87
|
58 test-AB→split {_} {A} {B} = refl
|
|
69
|
59
|
|
65
|
60 open RegularLanguage
|
|
|
61 isRegular : {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage Σ ) → Set
|
|
|
62 isRegular A x r = A x ≡ contain r x
|
|
|
63
|
|
73
|
64 postulate
|
|
|
65 fin-× : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A × B) {a * b}
|
|
|
66
|
|
65
|
67 M-Union : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
68 M-Union {Σ} A B = record {
|
|
|
69 states = states A × states B
|
|
|
70 ; astart = ( astart A , astart B )
|
|
73
|
71 ; aℕ = aℕ A * aℕ B
|
|
|
72 ; afin = fin-× (afin A) (afin B)
|
|
65
|
73 ; automaton = record {
|
|
|
74 δ = λ q x → ( δ (automaton A) (proj₁ q) x , δ (automaton B) (proj₂ q) x )
|
|
|
75 ; aend = λ q → ( aend (automaton A) (proj₁ q) \/ aend (automaton B) (proj₂ q) )
|
|
|
76 }
|
|
|
77 }
|
|
|
78
|
|
|
79 closed-in-union : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
|
|
|
80 closed-in-union A B [] = lemma where
|
|
|
81 lemma : aend (automaton A) (astart A) \/ aend (automaton B) (astart B) ≡
|
|
|
82 aend (automaton A) (astart A) \/ aend (automaton B) (astart B)
|
|
|
83 lemma = refl
|
|
|
84 closed-in-union {Σ} A B ( h ∷ t ) = lemma1 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
|
|
|
85 lemma1 : (t : List Σ) → (qa : states A ) → (qb : states B ) →
|
|
|
86 accept (automaton A) qa t \/ accept (automaton B) qb t
|
|
|
87 ≡ accept (automaton (M-Union A B)) (qa , qb) t
|
|
|
88 lemma1 [] qa qb = refl
|
|
|
89 lemma1 (h ∷ t ) qa qb = lemma1 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
|
|
|
90
|
|
|
91 -- M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
92 -- M-Concat {Σ} A B = record {
|
|
|
93 -- states = states A ∨ states B
|
|
|
94 -- ; astart = case1 (astart A )
|
|
|
95 -- ; automaton = record {
|
|
|
96 -- δ = {!!}
|
|
|
97 -- ; aend = {!!}
|
|
|
98 -- }
|
|
|
99 -- }
|
|
|
100 --
|
|
|
101 -- closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
|
|
|
102 -- closed-in-concat = {!!}
|
|
70
|
103
|
|
|
104 open import nfa
|
|
|
105 open import sbconst2
|
|
|
106 open FiniteSet
|
|
86
|
107 open import Data.Nat.Properties hiding ( _≟_ )
|
|
70
|
108 open import Relation.Binary as B hiding (Decidable)
|
|
|
109
|
|
73
|
110 postulate
|
|
|
111 fin-∨ : {A B : Set} → { a b : ℕ } → FiniteSet A {a} → FiniteSet B {b} → FiniteSet (A ∨ B) {a + b}
|
|
|
112 fin→ : {A : Set} → { a : ℕ } → FiniteSet A {a} → FiniteSet (A → Bool ) {exp 2 a}
|
|
70
|
113
|
|
|
114 Concat-NFA : {Σ : Set} → (A B : RegularLanguage Σ ) → NAutomaton (states A ∨ states B) Σ
|
|
86
|
115 Concat-NFA {Σ} A B = record { Nδ = δnfa ; Nend = nend }
|
|
|
116 module Concat-NFA where
|
|
70
|
117 δnfa : states A ∨ states B → Σ → states A ∨ states B → Bool
|
|
|
118 δnfa (case1 q) i (case1 q₁) = equal? (afin A) (δ (automaton A) q i) q₁
|
|
88
|
119 δnfa (case1 qa) i (case2 qb) = (aend (automaton A) qa ) /\
|
|
|
120 (equal? (afin B) qb (δ (automaton B) (astart B) i) )
|
|
70
|
121 δnfa (case2 q) i (case2 q₁) = equal? (afin B) (δ (automaton B) q i) q₁
|
|
|
122 δnfa _ i _ = false
|
|
|
123 nend : states A ∨ states B → Bool
|
|
|
124 nend (case2 q) = aend (automaton B) q
|
|
88
|
125 nend (case1 q) = aend (automaton A) q /\ aend (automaton B) (astart B) -- empty B case
|
|
70
|
126
|
|
|
127 Concat-NFA-start : {Σ : Set} → (A B : RegularLanguage Σ ) → states A ∨ states B → Bool
|
|
75
|
128 Concat-NFA-start A B q = equal? (fin-∨ (afin A) (afin B)) (case1 (astart A)) q
|
|
70
|
129
|
|
|
130 M-Concat : {Σ : Set} → (A B : RegularLanguage Σ ) → RegularLanguage Σ
|
|
|
131 M-Concat {Σ} A B = record {
|
|
|
132 states = states A ∨ states B → Bool
|
|
|
133 ; astart = Concat-NFA-start A B
|
|
|
134 ; aℕ = finℕ finf
|
|
|
135 ; afin = finf
|
|
|
136 ; automaton = subset-construction fin (Concat-NFA A B) (case1 (astart A))
|
|
|
137 } where
|
|
|
138 fin : FiniteSet (states A ∨ states B ) {aℕ A + aℕ B}
|
|
|
139 fin = fin-∨ (afin A) (afin B)
|
|
|
140 finf : FiniteSet (states A ∨ states B → Bool )
|
|
|
141 finf = fin→ fin
|
|
|
142
|
|
72
|
143 record Split {Σ : Set} (A : List Σ → Bool ) ( B : List Σ → Bool ) (x : List Σ ) : Set where
|
|
|
144 field
|
|
|
145 sp0 : List Σ
|
|
|
146 sp1 : List Σ
|
|
|
147 sp-concat : sp0 ++ sp1 ≡ x
|
|
|
148 prop0 : A sp0 ≡ true
|
|
|
149 prop1 : B sp1 ≡ true
|
|
|
150
|
|
|
151 open Split
|
|
|
152
|
|
|
153 list-empty++ : {Σ : Set} → (x y : List Σ) → x ++ y ≡ [] → (x ≡ [] ) ∧ (y ≡ [] )
|
|
|
154 list-empty++ [] [] refl = record { proj1 = refl ; proj2 = refl }
|
|
|
155 list-empty++ [] (x ∷ y) ()
|
|
|
156 list-empty++ (x ∷ x₁) y ()
|
|
|
157
|
|
|
158 open _∧_
|
|
|
159
|
|
74
|
160 open import Relation.Binary.PropositionalEquality hiding ( [_] )
|
|
71
|
161
|
|
74
|
162 c-split-lemma : {Σ : Set} → (A B : List Σ → Bool ) → (h : Σ) → ( t : List Σ ) → split A B (h ∷ t ) ≡ true
|
|
|
163 → ( ¬ (A [] ≡ true )) ∨ ( ¬ (B ( h ∷ t ) ≡ true) )
|
|
|
164 → split (λ t1 → A (h ∷ t1)) B t ≡ true
|
|
|
165 c-split-lemma {Σ} A B h t eq (case1 ¬p ) = sym ( begin
|
|
|
166 true
|
|
|
167 ≡⟨ sym eq ⟩
|
|
|
168 split A B (h ∷ t )
|
|
|
169 ≡⟨⟩
|
|
|
170 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
|
|
|
171 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-1 (¬-bool-t ¬p)) ⟩
|
|
|
172 false \/ split (λ t1 → A (h ∷ t1)) B t
|
|
|
173 ≡⟨ bool-or-1 refl ⟩
|
|
|
174 split (λ t1 → A (h ∷ t1)) B t
|
|
|
175 ∎ ) where open ≡-Reasoning
|
|
|
176 c-split-lemma {Σ} A B h t eq (case2 ¬p ) = sym ( begin
|
|
|
177 true
|
|
|
178 ≡⟨ sym eq ⟩
|
|
|
179 split A B (h ∷ t )
|
|
|
180 ≡⟨⟩
|
|
|
181 A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t
|
|
|
182 ≡⟨ cong ( λ k → k \/ split (λ t1 → A (h ∷ t1)) B t ) (bool-and-2 (¬-bool-t ¬p)) ⟩
|
|
|
183 false \/ split (λ t1 → A (h ∷ t1)) B t
|
|
|
184 ≡⟨ bool-or-1 refl ⟩
|
|
|
185 split (λ t1 → A (h ∷ t1)) B t
|
|
|
186 ∎ ) where open ≡-Reasoning
|
|
|
187
|
|
87
|
188 split→AB : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → split A B x ≡ true → Split A B x
|
|
|
189 split→AB {Σ} A B [] eq with bool-≡-? (A []) true | bool-≡-? (B []) true
|
|
|
190 split→AB {Σ} A B [] eq | yes eqa | yes eqb =
|
|
73
|
191 record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = eqa ; prop1 = eqb }
|
|
87
|
192 split→AB {Σ} A B [] eq | yes p | no ¬p = ⊥-elim (lemma-∧-1 eq (¬-bool-t ¬p ))
|
|
|
193 split→AB {Σ} A B [] eq | no ¬p | t = ⊥-elim (lemma-∧-0 eq (¬-bool-t ¬p ))
|
|
|
194 split→AB {Σ} A B (h ∷ t ) eq with bool-≡-? (A []) true | bool-≡-? (B (h ∷ t )) true
|
|
74
|
195 ... | yes px | yes py = record { sp0 = [] ; sp1 = h ∷ t ; sp-concat = refl ; prop0 = px ; prop1 = py }
|
|
87
|
196 ... | no px | _ with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case1 px) )
|
|
74
|
197 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
|
|
87
|
198 split→AB {Σ} A B (h ∷ t ) eq | _ | no px with split→AB (λ t1 → A ( h ∷ t1 )) B t (c-split-lemma A B h t eq (case2 px) )
|
|
74
|
199 ... | S = record { sp0 = h ∷ sp0 S ; sp1 = sp1 S ; sp-concat = cong ( λ k → h ∷ k) (sp-concat S) ; prop0 = prop0 S ; prop1 = prop1 S }
|
|
|
200
|
|
87
|
201 AB→split : {Σ : Set} → (A B : List Σ → Bool ) → ( x y : List Σ ) → A x ≡ true → B y ≡ true → split A B (x ++ y ) ≡ true
|
|
|
202 AB→split {Σ} A B [] [] eqa eqb = begin
|
|
74
|
203 split A B []
|
|
|
204 ≡⟨⟩
|
|
|
205 A [] /\ B []
|
|
|
206 ≡⟨ cong₂ (λ j k → j /\ k ) eqa eqb ⟩
|
|
|
207 true
|
|
|
208 ∎ where open ≡-Reasoning
|
|
87
|
209 AB→split {Σ} A B [] (h ∷ y ) eqa eqb = begin
|
|
74
|
210 split A B (h ∷ y )
|
|
|
211 ≡⟨⟩
|
|
|
212 A [] /\ B (h ∷ y) \/ split (λ t1 → A (h ∷ t1)) B y
|
|
|
213 ≡⟨ cong₂ (λ j k → j /\ k \/ split (λ t1 → A (h ∷ t1)) B y ) eqa eqb ⟩
|
|
|
214 true /\ true \/ split (λ t1 → A (h ∷ t1)) B y
|
|
|
215 ≡⟨⟩
|
|
|
216 true \/ split (λ t1 → A (h ∷ t1)) B y
|
|
|
217 ≡⟨⟩
|
|
|
218 true
|
|
|
219 ∎ where open ≡-Reasoning
|
|
87
|
220 AB→split {Σ} A B (h ∷ t) y eqa eqb = begin
|
|
74
|
221 split A B ((h ∷ t) ++ y)
|
|
|
222 ≡⟨⟩
|
|
|
223 A [] /\ B (h ∷ t ++ y) \/ split (λ t1 → A (h ∷ t1)) B (t ++ y)
|
|
|
224 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) ( begin
|
|
|
225 split (λ t1 → A (h ∷ t1)) B (t ++ y)
|
|
87
|
226 ≡⟨ AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ⟩
|
|
74
|
227 true
|
|
|
228 ∎ ) ⟩
|
|
|
229 A [] /\ B (h ∷ t ++ y) \/ true
|
|
|
230 ≡⟨ bool-or-3 ⟩
|
|
|
231 true
|
|
|
232 ∎ where open ≡-Reasoning
|
|
|
233
|
|
75
|
234 open NAutomaton
|
|
89
|
235 open import Data.List.Properties
|
|
70
|
236
|
|
71
|
237 closed-in-concat : {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x ( M-Concat A B )
|
|
87
|
238 closed-in-concat {Σ} A B x = ≡-Bool-func closed-in-concat→ closed-in-concat← where
|
|
|
239 finab = (fin-∨ (afin A) (afin B))
|
|
76
|
240 NFA = (Concat-NFA A B)
|
|
|
241 abmove : (q : states A ∨ states B) → (h : Σ ) → states A ∨ states B
|
|
|
242 abmove (case1 q) h = case1 (δ (automaton A) q h)
|
|
|
243 abmove (case2 q) h = case2 (δ (automaton B) q h)
|
|
88
|
244 lemma-nmove-ab : (q : states A ∨ states B) → (h : Σ ) → Nδ NFA q h (abmove q h) ≡ true
|
|
|
245 lemma-nmove-ab (case1 q) _ = equal?-refl (afin A)
|
|
|
246 lemma-nmove-ab (case2 q) _ = equal?-refl (afin B)
|
|
76
|
247 nmove : (q : states A ∨ states B) (nq : states A ∨ states B → Bool ) → (nq q ≡ true) → ( h : Σ ) →
|
|
87
|
248 exists finab (λ qn → nq qn /\ Nδ NFA qn h (abmove q h)) ≡ true
|
|
88
|
249 nmove (case1 q) nq nqt h = found finab (case1 q) ( bool-and-tt nqt (lemma-nmove-ab (case1 q) h) )
|
|
100
|
250 nmove (case2 q) nq nqt h = found finab (case2 q) ( bool-and-tt nqt (lemma-nmove-ab (case2 q) h) )
|
|
88
|
251 acceptB : (z : List Σ) → (q : states B) → (nq : states A ∨ states B → Bool ) → (nq (case2 q) ≡ true) → ( accept (automaton B) q z ≡ true )
|
|
87
|
252 → Naccept NFA finab nq z ≡ true
|
|
88
|
253 acceptB [] q nq nqt fb = lemma8 where
|
|
87
|
254 lemma8 : exists finab ( λ q → nq q /\ Nend NFA q ) ≡ true
|
|
88
|
255 lemma8 = found finab (case2 q) ( bool-and-tt nqt fb )
|
|
|
256 acceptB (h ∷ t ) q nq nq=q fb = acceptB t (δ (automaton B) q h) (Nmoves NFA finab nq h) (nmove (case2 q) nq nq=q h) fb
|
|
|
257 acceptA : (y z : List Σ) → (q : states A) → (nq : states A ∨ states B → Bool ) → (nq (case1 q) ≡ true)
|
|
75
|
258 → ( accept (automaton A) q y ≡ true ) → ( accept (automaton B) (astart B) z ≡ true )
|
|
87
|
259 → Naccept NFA finab nq (y ++ z) ≡ true
|
|
88
|
260 acceptA [] [] q nq nqt fa fb = found finab (case1 q) (bool-and-tt nqt (bool-and-tt fa fb ))
|
|
|
261 acceptA [] (h ∷ z) q nq nq=q fa fb = acceptB z nextb (Nmoves NFA finab nq h) lemma70 fb where
|
|
87
|
262 nextb : states B
|
|
|
263 nextb = δ (automaton B) (astart B) h
|
|
|
264 lemma70 : exists finab (λ qn → nq qn /\ Nδ NFA qn h (case2 nextb)) ≡ true
|
|
88
|
265 lemma70 = found finab (case1 q) ( bool-and-tt nq=q (bool-and-tt fa (lemma-nmove-ab (case2 (astart B)) h) ))
|
|
|
266 acceptA (h ∷ t) z q nq nq=q fa fb = acceptA t z (δ (automaton A) q h) (Nmoves NFA finab nq h) (nmove (case1 q) nq nq=q h) fa fb where
|
|
|
267 acceptAB : Split (contain A) (contain B) x
|
|
87
|
268 → Naccept NFA finab (equal? finab (case1 (astart A))) x ≡ true
|
|
88
|
269 acceptAB S = subst ( λ k → Naccept NFA finab (equal? finab (case1 (astart A))) k ≡ true ) ( sp-concat S )
|
|
|
270 (acceptA (sp0 S) (sp1 S) (astart A) (equal? finab (case1 (astart A))) (equal?-refl finab) (prop0 S) (prop1 S) )
|
|
87
|
271
|
|
|
272 closed-in-concat→ : Concat (contain A) (contain B) x ≡ true → contain (M-Concat A B) x ≡ true
|
|
|
273 closed-in-concat→ concat with split→AB (contain A) (contain B) x concat
|
|
75
|
274 ... | S = begin
|
|
87
|
275 accept (subset-construction finab NFA (case1 (astart A))) (Concat-NFA-start A B ) x
|
|
|
276 ≡⟨ ≡-Bool-func (subset-construction-lemma← finab NFA (case1 (astart A)) x )
|
|
|
277 (subset-construction-lemma→ finab NFA (case1 (astart A)) x ) ⟩
|
|
|
278 Naccept NFA finab (equal? finab (case1 (astart A))) x
|
|
88
|
279 ≡⟨ acceptAB S ⟩
|
|
75
|
280 true
|
|
|
281 ∎ where open ≡-Reasoning
|
|
87
|
282
|
|
92
|
283 open Found
|
|
99
|
284
|
|
101
|
285 data AB-state (nq : states A ∨ states B → Bool ) (qa : states A) (x : List Σ) : Set (Level.suc Level.zero) where
|
|
|
286 state-A : ((q : states A ∨ states B ) → nq q ≡ true → q ≡ case1 qa ) → AB-state nq qa x
|
|
|
287 state-AB : ((q : states A ∨ states B ) → ( nq q ≡ true ) →
|
|
|
288 ( (q ≡ case1 qa) ∨ ({qb : states B} → nq (case2 qb) ≡ true → ( accept (automaton B) qb x ≡ false ) ))) → AB-state nq qa x
|
|
99
|
289
|
|
101
|
290 open AB-state
|
|
100
|
291 contain-A : (x : List Σ) → (nq : states A ∨ states B → Bool ) → (fn : Naccept NFA finab nq x ≡ true )
|
|
101
|
292 → (qa : states A ) → AB-state nq qa x
|
|
94
|
293 → split (accept (automaton A) qa ) (contain B) x ≡ true
|
|
101
|
294 contain-A [] nq fn qa cond with found← finab fn | found-q (found← finab fn) | cond | inspect found-q (found← finab fn)
|
|
|
295 contain-A [] nq fn qa cond | S | s | state-A nq=t | record { eq = refl } with nq=t (found-q S) (bool-∧→tt-0 (found-p S))
|
|
|
296 ... | refl = bool-∧→tt-1 (found-p S)
|
|
|
297 contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ with cond-b (found-q S) (bool-∧→tt-0 (found-p S))
|
|
|
298 contain-A [] nq fn qa cond | S | s | state-AB cond-b | _ | case1 refl = bool-∧→tt-1 (found-p S)
|
|
|
299 contain-A [] nq fn qa cond | S | case2 qb | state-AB cond-b | record { eq = refl } | case2 accept-B = ⊥-elim ( lemma11 accept-B ) where
|
|
|
300 lemma11 : ( nq (case2 qb ) ≡ true → aend (automaton B) qb ≡ false ) → ⊥
|
|
|
301 lemma11 accept-B = ¬-bool ( accept-B (bool-∧→tt-0 (found-p S))) (bool-∧→tt-1 (found-p S ))
|
|
|
302 contain-A [] nq fn qa cond | S | case1 qa' | state-AB cond-b | record { eq = refl } | case2 accept-B = {!!}
|
|
100
|
303 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true
|
|
95
|
304 ... | yes eq = bool-or-41 eq
|
|
100
|
305 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA finab nq h) fn (δ (automaton A) qa h) {!!} ) where
|
|
87
|
306
|
|
|
307 lemma10 : Naccept NFA finab (equal? finab (case1 (astart A))) x ≡ true → split (contain A) (contain B) x ≡ true
|
|
100
|
308 lemma10 CC = contain-A x (Concat-NFA-start A B ) CC (astart A) {!!} where
|
|
87
|
309
|
|
|
310 closed-in-concat← : contain (M-Concat A B) x ≡ true → Concat (contain A) (contain B) x ≡ true
|
|
|
311 closed-in-concat← C with subset-construction-lemma← finab NFA (case1 (astart A)) x C
|
|
|
312 ... | CC = lemma10 CC
|
|
|
313
|
|
71
|
314
|
|
|
315
|
|
87
|
316
|
