Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/nfa.agda @ 405:af8f630b7e60

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 24 Sep 2023 18:02:04 +0900
parents 6f3636fbc481
children a60132983557
comparison
equal deleted inserted replaced
404:dfaf230f7b9a 405:af8f630b7e60
252 bool-1t : {b : Bool } → b ≡ true → (b /\ true) ≡ true 252 bool-1t : {b : Bool } → b ≡ true → (b /\ true) ≡ true
253 bool-1t refl = refl 253 bool-1t refl = refl
254 254
255 to-list1 : {Q : Set } (qs : Q → Bool ) → (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ qs all ) ≡ true 255 to-list1 : {Q : Set } (qs : Q → Bool ) → (all : List Q) → foldr (λ q x → qs q /\ x ) true (ssQ qs all ) ≡ true
256 to-list1 qs [] = refl 256 to-list1 qs [] = refl
257 to-list1 qs (x ∷ all) with qs x | inspect qs x 257 to-list1 qs (x ∷ all) with qs x in eq
258 ... | false | record { eq = eq } = to-list1 qs all 258 ... | false = to-list1 qs all
259 ... | true | record { eq = eq } = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) ) 259 ... | true = subst (λ k → k /\ foldr (λ q → _/\_ (qs q)) true (ssQ qs all) ≡ true ) (sym eq) ( bool-t1 (to-list1 qs all) )
260 260
261 existsS1-valid : ¬ ( (qs : States1 → Bool ) → ( existsS1 qs ≡ true ) ) 261 existsS1-valid : ¬ ( (qs : States1 → Bool ) → ( existsS1 qs ≡ true ) )
262 existsS1-valid n = ¬-bool refl ( n ( λ x → false )) 262 existsS1-valid n = ¬-bool refl ( n ( λ x → false ))
263 263