Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/regular-concat.agda @ 270:dd98e7e5d4a5
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 |
line wrap: on
line diff
--- a/automaton-in-agda/src/regular-concat.agda Fri Nov 26 09:58:19 2021 +0900 +++ b/automaton-in-agda/src/regular-concat.agda Fri Nov 26 20:02:06 2021 +0900 @@ -203,7 +203,7 @@ contain-A (h ∷ t) nq fn qa cond with bool-≡-? ((aend (automaton A) qa) /\ accept (automaton B) (δ (automaton B) (astart B) h) t ) true ... | yes eq = bool-or-41 eq -- found A ++ B all end ... | 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 - --- prove ab-ase condition (we haven't checked but case2 b may happen) + --- prove ab-case condition (we haven't checked but case2 b may happen) 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 lemma11 (case1 qa') ex with found← finab ex ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S))