Mercurial > hg > Members > kono > Proof > automaton
changeset 51:bc0400528027
flcagl finish
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Sun, 07 Apr 2019 18:22:16 +0900 |
| parents | 62ad890b6cc7 |
| children | 8438c989d5a7 |
| files | agda/flcagl.agda |
| diffstat | 1 files changed, 36 insertions(+), 14 deletions(-) [+] |
line wrap: on
line diff
--- a/agda/flcagl.agda Sat Apr 06 22:01:18 2019 +0900 +++ b/agda/flcagl.agda Sun Apr 07 18:22:16 2019 +0900 @@ -193,7 +193,7 @@ ≅δ (concat-union-distribr k) a with ν k ≅δ (concat-union-distribr k {l} {m}) a | true = begin δ k a · (l ∪ m) ∪ (δ l a ∪ δ m a) - ≈⟨ union-congl (concat-union-distribr (δ k a)) ⟩ + ≈⟨ union-congl (concat-union-distribr _) ⟩ (δ k a · l ∪ δ k a · m) ∪ (δ l a ∪ δ m a) ≈⟨ union-swap24 ⟩ (δ k a · l ∪ δ l a) ∪ (δ k a · m ∪ δ m a) @@ -208,9 +208,11 @@ ≅δ (concat-union-distribl k {l} {m}) a | false | true = begin (if false ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩ - (δ k a ∪ δ l a) · m ∪ δ m a - ≈⟨ {!!} ⟩ - δ k a · m ∪ ( δ l a · m ∪ δ m a ) + ((δ k a ∪ δ l a) · m ) ∪ δ m a + ≈⟨ union-congl (concat-union-distribl _) ⟩ + (δ k a · m ∪ δ l a · m) ∪ δ m a + ≈⟨ union-assoc _ ⟩ + (δ k a · m) ∪ ( δ l a · m ∪ δ m a ) ≈⟨ ≅refl ⟩ (if false then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m) ∎ @@ -218,8 +220,14 @@ ≅δ (concat-union-distribl k {l} {m}) a | true | false = begin (if true ∨ false then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩ - (δ k a ∪ δ l a) · m ∪ δ m a - ≈⟨ {!!} ⟩ + ((δ k a ∪ δ l a) · m ) ∪ δ m a + ≈⟨ union-congl (concat-union-distribl _) ⟩ + (δ k a · m ∪ δ l a · m) ∪ δ m a + ≈⟨ union-assoc _ ⟩ + δ k a · m ∪ ( δ l a · m ∪ δ m a ) + ≈⟨ union-congr ( union-comm _ _) ⟩ + δ k a · m ∪ δ m a ∪ δ l a · m + ≈⟨ ≅sym ( union-assoc _ ) ⟩ (δ k a · m ∪ δ m a) ∪ δ l a · m ≈⟨ ≅refl ⟩ ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if false then δ l a · m ∪ δ m a else δ l a · m)) @@ -229,7 +237,21 @@ (if true ∨ true then (δ k a ∪ δ l a) · m ∪ δ m a else (δ k a ∪ δ l a) · m) ≈⟨ ≅refl ⟩ (δ k a ∪ δ l a) · m ∪ δ m a - ≈⟨ {!!} ⟩ + ≈⟨ union-congl ( concat-union-distribl _ ) ⟩ + (δ k a · m ∪ δ l a · m) ∪ δ m a + ≈⟨ union-assoc _ ⟩ + δ k a · m ∪ ( δ l a · m ∪ δ m a ) + ≈⟨ ≅sym ( union-congr ( union-congr ( union-idem _ ) ) ) ⟩ + δ k a · m ∪ ( δ l a · m ∪ (δ m a ∪ δ m a) ) + ≈⟨ ≅sym ( union-congr ( union-assoc _ )) ⟩ + δ k a · m ∪ ( (δ l a · m ∪ δ m a ) ∪ δ m a ) + ≈⟨ union-congr ( union-congl ( union-comm _ _) ) ⟩ + δ k a · m ∪ ( (δ m a ∪ δ l a · m ) ∪ δ m a ) + ≈⟨ ≅sym ( union-assoc _ ) ⟩ + ( δ k a · m ∪ (δ m a ∪ δ l a · m )) ∪ δ m a + ≈⟨ ≅sym ( union-congl ( union-assoc _ ) ) ⟩ + ((δ k a · m ∪ δ m a) ∪ δ l a · m) ∪ δ m a + ≈⟨ union-assoc _ ⟩ (δ k a · m ∪ δ m a) ∪ δ l a · m ∪ δ m a ≈⟨ ≅refl ⟩ ((if true then δ k a · m ∪ δ m a else δ k a · m) ∪ (if true then δ l a · m ∪ δ m a else δ l a · m)) @@ -258,15 +280,15 @@ concat-assoc : ∀{i} (k {l m} : Lang ∞) → (k · l) · m ≅⟨ i ⟩≅ k · (l · m) ≅ν (concat-assoc {i} k {l} {m} ) = ∧-assoc ( ν k ) ( ν l ) ( ν m ) ≅δ (concat-assoc {i} k {l} {m} ) a with ν k - ≅δ (concat-assoc {i} k {l} {m}) a | false = concat-assoc (δ k a) + ≅δ (concat-assoc {i} k {l} {m}) a | false = concat-assoc _ ≅δ (concat-assoc {i} k {l} {m}) a | true with ν l ≅δ (concat-assoc {i} k {l} {m}) a | true | false = begin ( if false then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m ) ≈⟨ ≅refl ⟩ (δ k a · l ∪ δ l a) · m - ≈⟨ concat-union-distribl (δ k a · l) ⟩ + ≈⟨ concat-union-distribl _ ⟩ ((δ k a · l) · m ) ∪ ( δ l a · m ) - ≈⟨ union-congl (concat-assoc (δ k a)) ⟩ + ≈⟨ union-congl (concat-assoc _) ⟩ (δ k a · l · m ) ∪ ( δ l a · m ) ≈⟨ ≅refl ⟩ δ k a · l · m ∪ (if false then δ l a · m ∪ δ m a else δ l a · m) @@ -275,11 +297,11 @@ (if true then (δ k a · l ∪ δ l a) · m ∪ δ m a else (δ k a · l ∪ δ l a) · m) ≈⟨ ≅refl ⟩ ((( δ k a · l ) ∪ δ l a) · m ) ∪ δ m a - ≈⟨ union-congl (concat-union-distribl (δ k a · l) ) ⟩ + ≈⟨ union-congl (concat-union-distribl _ ) ⟩ ((δ k a · l) · m ∪ ( δ l a · m )) ∪ δ m a - ≈⟨ union-congl ( union-congl (concat-assoc (δ k a))) ⟩ + ≈⟨ union-congl ( union-congl (concat-assoc _)) ⟩ (( δ k a · l · m ) ∪ ( δ l a · m )) ∪ δ m a - ≈⟨ union-assoc ( δ k a · l · m ) ⟩ + ≈⟨ union-assoc _ ⟩ ( δ k a · l · m ) ∪ ( ( δ l a · m ) ∪ δ m a ) ≈⟨ ≅refl ⟩ δ k a · l · m ∪ (if true then δ l a · m ∪ δ m a else δ l a · m) @@ -322,7 +344,7 @@ δ k a · l ∪ δ m a ≈⟨ union-congl (concat-congr (star-from-rec k {l} {m} n p)) ⟩ (δ k a · (k * · m) ∪ δ m a) - ≈⟨ union-congl (≅sym (concat-assoc (δ k a))) ⟩ + ≈⟨ union-congl (≅sym (concat-assoc _)) ⟩ (δ k a · (k *)) · m ∪ δ m a ∎ where open EqR (Bis _)