Mercurial > hg > Members > kono > Proof > automaton

changeset 110:795850729aaa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
clean up
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 17 Nov 2019 18:07:47 +0900
parents 330fa494f0e8
children ed0a2dad62f4
files agda/regular-language.agda
diffstat 1 files changed, 3 insertions(+), 5 deletions(-) [+]
line wrap: on
line diff
--- a/agda/regular-language.agda	Sun Nov 17 17:47:59 2019 +0900
+++ b/agda/regular-language.agda	Sun Nov 17 18:07:47 2019 +0900
@@ -305,11 +305,9 @@
        lemma11 (case2 qb)  ex with found← finab ex 
        ... | S with found-q S | inspect found-q S | cond (found-q S) (bool-∧→tt-0 (found-p S)) 
        lemma11 (case2 qb)  ex | S | case2 qb' | record { eq = refl } | nb =
-               contra-position (λ fb → subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb ) nb where
-           lemma13 : accept (automaton B) qb' (h ∷ t) ≡ true → ⊥
-           lemma13 = nb
-           lemma14 : nq (case2 qb') /\ equal? (afin B) (δ (automaton B) qb' h) qb ≡ true
-           lemma14 = found-p S
+               contra-position lemma13 nb where
+           lemma13 :  accept (automaton B) qb t ≡ true → accept (automaton B) qb' (h ∷ t) ≡ true
+           lemma13 fb = subst (λ k → accept (automaton B) k t ≡ true ) (sym (equal→refl (afin B) (bool-∧→tt-1 (found-p S)))) fb  
        lemma11 (case2 qb)  ex | S | case1 qa | record { eq = refl } | refl with bool-∧→tt-1 (found-p S)
        ... | eee = contra-position lemma12 ne where
            lemma12 : accept (automaton B) qb t ≡ true → aend (automaton A) qa /\ accept (automaton B) (δ (automaton B) (astart B) h) t ≡ true