Mercurial > hg > Members > kono > Proof > automaton

comparison automaton-in-agda/src/regular-language.agda @ 409:4e4acdc43dee

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 Thu, 16 Nov 2023 17:40:42 +0900
parents 3d0aa205edf9
children db02b6938e04
comparison
equal deleted inserted replaced
408:3d0aa205edf9 409:4e4acdc43dee
205 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩ 205 ≡⟨ cong ( λ k → A [] /\ B (h ∷ t ++ y) \/ k ) (AB→split {Σ} (λ t1 → A (h ∷ t1)) B t y eqa eqb ) ⟩
206 A [] /\ B (h ∷ t ++ y) \/ true ≡⟨ bool-or-3 ⟩ 206 A [] /\ B (h ∷ t ++ y) \/ true ≡⟨ bool-or-3 ⟩
207 true ∎ where open ≡-Reasoning 207 true ∎ where open ≡-Reasoning
208 208
209 209
210 -- plit→AB1 : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x → split A B x ≡ true 210 split→AB1 : {Σ : Set} → (A B : List Σ → Bool ) → ( x : List Σ ) → Split A B x → split A B x ≡ true
211 -- plit→AB1 {Σ} A B [] S = begin 211 split→AB1 {Σ} A B x S = subst (λ k → split A B k ≡ true ) (sp-concat S) ( AB→split A B _ _ (prop0 S) (prop1 S) )
212 -- split A B [] ≡⟨⟩ 212
213 -- A [] /\ B [] ≡⟨ cong₂ _/\_ a=t b=t ⟩ 213
214 -- true /\ true ≡⟨ bool-and-tt refl refl ⟩
215 -- true ∎ where
216 -- open ≡-Reasoning
217 -- a=t : A [] ≡ true
218 -- a=t = begin
219 -- A [] ≡⟨ cong (λ k → A k) (sym (proj1 (list-empty++ (sp0 S) (sp1 S) (sp-concat S)))) ⟩
220 -- A (sp0 S) ≡⟨ prop0 S ⟩
221 -- true ∎ where open ≡-Reasoning
222 -- b=t : B [] ≡ true
223 -- b=t = begin
224 -- B [] ≡⟨ cong (λ k → B k) (sym (proj2 (list-empty++ (sp0 S) (sp1 S) (sp-concat S)))) ⟩
225 -- B (sp1 S) ≡⟨ prop1 S ⟩
226 -- true ∎ where open ≡-Reasoning
227 -- plit→AB1 {Σ} A B (h ∷ t ) S = begin
228 -- split A B (h ∷ t ) ≡⟨⟩
229 -- A [] /\ B (h ∷ t) \/ split (λ t1 → A (h ∷ t1)) B t ≡⟨ cong (λ k → A [] /\ B (h ∷ t) \/ k )
230 -- (split→AB1 {Σ} (λ t1 → A (h ∷ t1)) B t ? ) ⟩
231 -- A [] /\ B (h ∷ t) \/ true ≡⟨ bool-or-3 ⟩
232 -- true ∎ where open ≡-Reasoning
233 --
234