Mercurial > hg > Members > kono > Proof > automaton
diff 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 |
line wrap: on
line diff
--- a/automaton-in-agda/src/non-regular.agda Thu Aug 10 09:59:47 2023 +0900 +++ b/automaton-in-agda/src/non-regular.agda Sun Sep 24 11:32:01 2023 +0900 @@ -312,7 +312,21 @@ count1 x + count1 y + count1 z ∎ where open ≡-Reasoning -- this takes very long time to check and needs 10GB bb22 : count0 y ≡ count1 y - bb22 = ? + bb22 = begin + count0 y ≡⟨ sym ( +-cancelʳ-≡ {count1 z + count0 x + count0 y + count0 z} (count1 y) (count0 y) (+-cancelˡ-≡ (count1 x + count1 y) ( + begin + count1 x + count1 y + (count1 y + (count1 z + count0 x + count0 y + count0 z)) ≡⟨ solve +-0-monoid ⟩ + (count1 x + count1 y + count1 y + count1 z) + (count0 x + count0 y + count0 z) ≡⟨ sym (cong₂ _+_ nn21 (sym nn20)) ⟩ + (count0 x + count0 y + count0 y + count0 z) + (count1 x + count1 y + count1 z) ≡⟨ +-comm _ (count1 x + count1 y + count1 z) ⟩ + (count1 x + count1 y + count1 z) + (count0 x + count0 y + count0 y + count0 z) ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + (count1 z + (count0 x + count0 y)) + count0 y + count0 z + ≡⟨ cong (λ k → count1 x + count1 y + (count1 z + k) + count0 y + count0 z) (+-comm (count0 x) _) ⟩ + count1 x + count1 y + (count1 z + (count0 y + count0 x)) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + ((count1 z + count0 y) + count0 x) + count0 y + count0 z + ≡⟨ cong (λ k → count1 x + count1 y + (k + count0 x) + count0 y + count0 z ) (+-comm (count1 z) _) ⟩ + count1 x + count1 y + (count0 y + count1 z + count0 x) + count0 y + count0 z ≡⟨ solve +-0-monoid ⟩ + count1 x + count1 y + (count0 y + (count1 z + count0 x + count0 y + count0 z)) ∎ ))) ⟩ + count1 y ∎ where open ≡-Reasoning -- -- y contains i0 and i1 , so we have i1 → i0 transition in y ++ y --