Mercurial > hg > Members > kono > Proof > automaton
comparison automaton-in-agda/src/non-regular.agda @ 403:c298981108c1
fix for std-lib 2.0
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 24 Sep 2023 11:32:01 +0900 |
| parents | 2e22a1f3a55a |
| children | af8f630b7e60 |
comparison
equal
deleted
inserted
replaced
| 402:093e386c10a2 | 403:c298981108c1 |
|---|---|
| 310 count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (distr1 y z) ⟩ | 310 count1 x + count1 (y ++ z) ≡⟨ cong (λ k → count1 x + k) (distr1 y z) ⟩ |
| 311 count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ | 311 count1 x + (count1 y + count1 z) ≡⟨ solve +-0-monoid ⟩ |
| 312 count1 x + count1 y + count1 z ∎ where open ≡-Reasoning | 312 count1 x + count1 y + count1 z ∎ where open ≡-Reasoning |
| 313 -- this takes very long time to check and needs 10GB | 313 -- this takes very long time to check and needs 10GB |
| 314 bb22 : count0 y ≡ count1 y | 314 bb22 : count0 y ≡ count1 y |
| 315 bb22 = ? | 315 bb22 = begin |
| 316 count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( | |
| 317 begin | |
| 318 count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ | |
| 319 (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ | |
| 320 (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ | |
| 321 (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ | |
| 322 count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z | |
| 323 ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ | |
| 324 count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ | |
| 325 count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z | |
| 326 ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ | |
| 327 count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ | |
| 328 count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ | |
| 329 count1 y ∎ where open ≡-Reasoning | |
| 316 -- | 330 -- |
| 317 -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y | 331 -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y |
| 318 -- | 332 -- |
| 319 bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) | 333 bb23 : count0 y ≡ count1 y → i1i0 (y ++ y) |
| 320 bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26) where | 334 bb23 eq = bb25 y y bb26 (subst (λ k → 0 < k ) (sym eq) bb26) where |