Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regular-concat.agda @ 270:dd98e7e5d4a5

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
derive worked but finiteness is difficult add regular star
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 26 Nov 2021 20:02:06 +0900
parents 52ed73a116d0
children 1c8ed1220489
comparison
equal deleted inserted replaced
269:52ed73a116d0 270:dd98e7e5d4a5
201 ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S) 201 ... | case1 qa' | record { eq = refl } | refl = bool-∧→tt-1 (found-p S)
202 ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S))) 202 ... | case2 qb | record { eq = refl } | ab = ⊥-elim ( ab (bool-∧→tt-1 (found-p S)))
203 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true 203 contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true
204 ... | yes eq = bool-or-41 eq -- found A ++ B all end 204 ... | yes eq = bool-or-41 eq -- found A ++ B all end
205 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion 205 ... | no ne = bool-or-31 (contain-A t (Nmoves NFA (CNFA-exist A B) nq h) fn (δ (automaton A) qa h) lemma11 ) where -- B failed continue with ab-base condtion
206 --- prove ab-ase condition (we haven't checked but case2 b may happen) 206 --- prove ab-case condition (we haven't checked but case2 b may happen)
207 lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t 207 lemma11 : (q : states A ∨ states B) → exists finab (λ qn → nq qn /\ Nδ NFA qn h q) ≡ true → ab-case q (δ (automaton A) qa h) t
208 lemma11 (case1 qa') ex with found← finab ex 208 lemma11 (case1 qa') ex with found← finab ex
209 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 209 ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))
210 ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) -- continued A case 210 ... | case1 qa | record { eq = refl } | refl = sym ( equal→refl (afin A) ( bool-∧→tt-1 (found-p S) )) -- continued A case
211 ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false 211 ... | case2 qb | record { eq = refl } | nb with bool-∧→tt-1 (found-p S) -- δnfa (case2 q) i (case1 q₁) is false