Mercurial > hg > Members > kono > Proof > automaton
diff automaton-in-agda/src/nfa.agda @ 405:af8f630b7e60
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 18:02:04 +0900 |
| parents | 6f3636fbc481 |
| children | a60132983557 |
line wrap: on
line diff
--- a/automaton-in-agda/src/nfa.agda Sun Sep 24 13:20:31 2023 +0900 +++ b/automaton-in-agda/src/nfa.agda Sun Sep 24 18:02:04 2023 +0900 @@ -254,9 +254,9 @@ to-list1 : {Q : Set } (qs : Q → Bool ) → (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ qs all ) ≡ true to-list1 qs [] = refl -to-list1 qs (x ∷ all) with qs x | inspect qs x -... | false | record { eq = eq } = to-list1 qs all -... | true | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) ) +to-list1 qs (x ∷ all) with qs x in eq +... | false = to-list1 qs all +... | true = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) ) existsS1-valid : ¬ ( (qs : States1 → Bool ) → ( existsS1 qs ≡ true ) ) existsS1-valid n = ¬-bool refl ( n ( λ x → false ))