# HG changeset patch
# User Shinji KONO <kono@ie.u-ryukyu.ac.jp>
# Date 1554555678 -32400
# Node ID 62ad890b6cc7a0eea1f1768fdbd45b50b6c455d5
# Parent  4135d56b81204979b94f5fdf5d5c0566cf02ade0
...

diff -r 4135d56b8120 -r 62ad890b6cc7 agda/flcagl.agda
--- a/agda/flcagl.agda	Sat Apr 06 21:06:02 2019 +0900
+++ b/agda/flcagl.agda	Sat Apr 06 22:01:18 2019 +0900
@@ -160,8 +160,6 @@
         infixr 6 _∪_
         infixr 7 _·_
         infix 5 _≅⟨_⟩≅_
-        postulate
-                concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
 
         union-congl : ∀{i}{k k′ l : Lang ∞}
              (p : k ≅⟨ i ⟩≅ k′) → ( k ∪ l ) ≅⟨ i ⟩≅ ( k′ ∪ l )
@@ -203,6 +201,41 @@
                where open EqR (Bis _)
         ≅δ (concat-union-distribr k) a | false = concat-union-distribr (δ k a)
 
+        concat-union-distribl : ∀{i} (k {l m} : Lang ∞) → ( k ∪ l ) · m ≅⟨ i ⟩≅ ( k · m ) ∪ ( l · m )
+        ≅ν (concat-union-distribl k {l} {m}) = ∧-distribʳ-∨ _ (ν k) _ 
+        ≅δ (concat-union-distribl k {l} {m}) a with ν k |  ν l 
+        ≅δ (concat-union-distribl k {l} {m}) a | false | false = concat-union-distribl (δ k a)
+        ≅δ (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 )
+           ≈⟨ ≅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)
+           ∎
+               where open EqR (Bis _)
+        ≅δ (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 · 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))
+           ∎
+               where open EqR (Bis _)
+        ≅δ (concat-union-distribl k {l} {m}) a | true | true = begin
+                (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
+           ≈⟨ {!!} ⟩
+                (δ 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))
+           ∎
+               where open EqR (Bis _)
+
         postulate
                 concat-emptyl : ∀{i} l → ∅ · l ≅⟨ i ⟩≅ ∅
                 concat-emptyr : ∀{i} l → l · ∅ ≅⟨ i ⟩≅ ∅