Prove satisfaction for concatenation.lemma3.5

4 files changed, 220 insertions, 89 deletions

diff --git a/src/Cfe/Language/Base.agda b/src/Cfe/Language/Base.agda
index 3e954b2..a3b5136 100644
--- a/src/Cfe/Language/Base.agda
+++ b/src/Cfe/Language/Base.agda
@@ -20,6 +20,8 @@ open import Relation.Binary.PropositionalEquality
 
 infix 4 _∈_
 infix 4 _∉_
+infix 4 _≈_
+infix 4 _≤_
 
 record Language a : Set (c ⊔ ℓ ⊔ suc a) where
   field
diff --git a/src/Cfe/Language/Construct/Concatenate.agda b/src/Cfe/Language/Construct/Concatenate.agda
index 8dff2ff..c4a5670 100644
--- a/src/Cfe/Language/Construct/Concatenate.agda
+++ b/src/Cfe/Language/Construct/Concatenate.agda
@@ -16,83 +16,15 @@ open import Data.Product as Product
 open import Data.Unit using (⊤)
 open import Function
 open import Level
-open import Relation.Binary.PropositionalEquality as ≡
+import Relation.Binary.PropositionalEquality as ≡
 open import Relation.Nullary
 open import Relation.Unary hiding (_∈_)
 import Relation.Binary.Indexed.Heterogeneous as I
 
 open Setoid over using () renaming (Carrier to C; _≈_ to _∼_; refl to ∼-refl; sym to ∼-sym; trans to ∼-trans)
 
-module _
-  {a b}
-  (A : Language a)
-  (B : Language b)
-  where
-
-  private
-    module A = Language A
-    module B = Language B
-
-  infix 7 _∙_
-
-  Concat : List C → Set (c ⊔ ℓ ⊔ a ⊔ b)
-  Concat l = ∃[ l₁ ] l₁ ∈ A × ∃[ l₂ ] l₂ ∈ B × l₁ ++ l₂ ≋ l
-
-  _∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b)
-  _∙_ = record
-    { 𝕃 = Concat
-    ; ∈-resp-≋ = λ { l≋l′ (_ , l₁∈A , _ , l₂∈B , eq) → -, l₁∈A , -, l₂∈B , ≋-trans eq l≋l′
-      }
-    }
-
-isMonoid : ∀ {a} → IsMonoid 𝕃._≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝)
-isMonoid {a} = record
-  { isSemigroup = record
-    { isMagma = record
-      { isEquivalence = ≈-isEquivalence
-      ; ∙-cong = λ X≈Y U≈V → record
-        { f = λ { (_ , l₁∈X , _ , l₂∈U , eq) → -, _≈_.f X≈Y l₁∈X , -, _≈_.f U≈V l₂∈U , eq }
-        ; f⁻¹ = λ { (_ , l₁∈Y , _ , l₂∈V , eq) → -, _≈_.f⁻¹ X≈Y l₁∈Y , -, _≈_.f⁻¹ U≈V l₂∈V , eq }
-        }
-      }
-    ; assoc = λ X Y Z → record
-      { f = λ {l} → λ { (l₁₂ , (l₁ , l₁∈X , l₂ , l₂∈Y , eq₁) , l₃ , l₃∈Z , eq₂) →
-        -, l₁∈X , -, (-, l₂∈Y , -, l₃∈Z , ≋-refl) , (begin
-          l₁ ++ l₂ ++ l₃ ≡˘⟨ ++-assoc l₁ l₂ l₃ ⟩
-          (l₁ ++ l₂) ++ l₃ ≈⟨ ++⁺ eq₁ ≋-refl ⟩
-          l₁₂ ++ l₃ ≈⟨ eq₂ ⟩
-          l ∎) }
-      ; f⁻¹ = λ {l} → λ { (l₁ , l₁∈X , l₂₃ , (l₂ , l₂∈Y , l₃ , l₃∈Z , eq₁) , eq₂) →
-        -, (-, l₁∈X , -, l₂∈Y , ≋-refl) , -, l₃∈Z , (begin
-          (l₁ ++ l₂) ++ l₃ ≡⟨ ++-assoc l₁ l₂ l₃ ⟩
-          l₁ ++ l₂ ++ l₃ ≈⟨ ++⁺ ≋-refl eq₁ ⟩
-          l₁ ++ l₂₃ ≈⟨ eq₂ ⟩
-          l ∎) }
-      }
-    }
-  ; identity = (λ X → record
-    { f = λ { ([] , _ , _ , l₂∈X , eq) → Language.∈-resp-≋ X eq l₂∈X }
-    ; f⁻¹ = λ l∈X → -, lift refl , -, l∈X , ≋-refl
-    }) , (λ X → record
-    { f = λ { (l₁ , l₁∈X , [] , _ , eq) → Language.∈-resp-≋ X (≋-trans (≋-reflexive (sym (++-identityʳ l₁))) eq) l₁∈X }
-    ; f⁻¹ = λ {l} l∈X → -, l∈X , -, lift refl , ≋-reflexive (++-identityʳ l)
-    })
-  }
-  where
-  open import Relation.Binary.Reasoning.Setoid ≋-setoid
-
-∙-mono : ∀ {a b} → _∙_ Preserves₂ _≤_ {a} ⟶ _≤_ {b} ⟶ _≤_
-∙-mono X≤Y U≤V = record
-  { f = λ {(_ , l₁∈X , _ , l₂∈U , eq) → -, X≤Y.f l₁∈X , -, U≤V.f l₂∈U , eq}
-  }
-  where
-  module X≤Y = _≤_ X≤Y
-  module U≤V = _≤_ U≤V
-
-private
+module Compare where
   data Compare : List C → List C → List C → List C → Set (c ⊔ ℓ) where
-    -- left : ∀ {ws₁ w ws₂ xs ys z zs₁ zs₂} → (ws₁≋ys : ws₁ ≋ ys) → (w∼z : w ∼ z) → (ws₂≋zs₁ : ws₂ ≋ zs₁) → (xs≋zs₂ : xs ≋ zs₂) → Compare (ws₁ ++ w ∷ ws₂) xs ys (z ∷ zs₁ ++ zs₂)
-    -- right : ∀ {ws x xs₁ xs₂ ys₁ y ys₂ zs} → (ws≋ys₁ : ws ≋ ys₁) → (x∼y : x ∼ y) → (xs₁≋ys₂ : xs₁ ≋ ys₂) → (xs₂≋zs : xs₂ ≋ zs) → Compare ws (x ∷ xs₁ ++ xs₂) (ys₁ ++ y ∷ ys₂) zs
     back : ∀ {xs zs} → (xs≋zs : xs ≋ zs) → Compare [] xs [] zs
     left : ∀ {w ws xs z zs} → Compare ws xs [] zs → (w∼z : w ∼ z) → Compare (w ∷ ws) xs [] (z ∷ zs)
     right : ∀ {x xs y ys zs} → Compare [] xs ys zs → (x∼y : x ∼ y) → Compare [] (x ∷ xs) (y ∷ ys) zs
@@ -142,29 +74,160 @@ private
   right-split (front cmp w∼y) r with right-split cmp r
   ... | (_ , _ , eq₁ , eq₂) = -, -, w∼y ∷ eq₁ , eq₂
 
-  eq-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isEqual cmp → ws ≋ ys
-  eq-split (back xs≋zs) e = []
-  eq-split (front cmp w∼y) e = w∼y ∷ eq-split cmp e
+  eq-split : ∀ {ws xs ys zs} → (cmp : Compare ws xs ys zs) → isEqual cmp → ws ≋ ys × xs ≋ zs
+  eq-split (back xs≋zs) e = [] , xs≋zs
+  eq-split (front cmp w∼y) e = map₁ (w∼y ∷_) (eq-split cmp e)
+
+module _
+  {a b}
+  (A : Language a)
+  (B : Language b)
+  where
+
+  private
+    module A = Language A
+    module B = Language B
+
+  infix 7 _∙_
+
+  record Concat (l : List C) : Set (c ⊔ ℓ ⊔ a ⊔ b) where
+    field
+      l₁ : List C
+      l₂ : List C
+      l₁∈A : l₁ ∈ A
+      l₂∈B : l₂ ∈ B
+      eq : l₁ ++ l₂ ≋ l
+
+  _∙_ : Language (c ⊔ ℓ ⊔ a ⊔ b)
+  _∙_ = record
+    { 𝕃 = Concat
+    ; ∈-resp-≋ = λ
+      { l≋l′ record { l₁ = _ ; l₂ = _ ; l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq } → record
+        { l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = ≋-trans eq l≋l′ }
+      }
+    }
+
+∙-cong : ∀ {a} → Congruent₂ _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+∙-cong X≈Y U≈V = record
+  { f = λ
+    { record { l₁∈A = l₁∈X ; l₂∈B = l₂∈Y ; eq = eq } → record
+      { l₁∈A = X≈Y.f l₁∈X
+      ; l₂∈B = U≈V.f l₂∈Y
+      ; eq = eq
+      }
+    }
+  ; f⁻¹ = λ
+    { record { l₁∈A = l₁∈Y ; l₂∈B = l₂∈V ; eq = eq } → record
+      { l₁∈A = X≈Y.f⁻¹ l₁∈Y
+      ; l₂∈B = U≈V.f⁻¹ l₂∈V
+      ; eq = eq
+      }
+    }
+  }
+  where
+  module X≈Y = _≈_ X≈Y
+  module U≈V = _≈_ U≈V
+
+∙-assoc : ∀ {a b c} (A : Language a) (B : Language b) (C : Language c) →
+          (A ∙ B) ∙ C ≈ A ∙ (B ∙ C)
+∙-assoc A B C = record
+  { f = λ
+    { record
+      { l₂ = l₃
+      ; l₁∈A = record { l₁ = l₁ ; l₂ = l₂ ; l₁∈A = l₁∈A ; l₂∈B = l₂∈B ; eq = eq₁ }
+      ; l₂∈B = l₃∈C
+      ; eq = eq₂
+      } → record
+      { l₁∈A = l₁∈A
+      ; l₂∈B = record
+        { l₁∈A = l₂∈B
+        ; l₂∈B = l₃∈C
+        ; eq = ≋-refl
+        }
+      ; eq = ≋-trans (≋-sym (≋-reflexive (++-assoc l₁ l₂ l₃))) (≋-trans (++⁺ eq₁ ≋-refl) eq₂)
+      }
+    }
+  ; f⁻¹ = λ
+    { record
+      { l₁ = l₁
+      ; l₁∈A = l₁∈A
+      ; l₂∈B = record { l₁ = l₂ ; l₂ = l₃ ; l₁∈A = l₂∈B ; l₂∈B = l₃∈C ; eq = eq₁ }
+      ; eq = eq₂
+      } → record
+      { l₁∈A = record
+        { l₁∈A = l₁∈A
+        ; l₂∈B = l₂∈B
+        ; eq = ≋-refl
+        }
+      ; l₂∈B = l₃∈C
+      ; eq = ≋-trans (≋-reflexive (++-assoc l₁ l₂ l₃)) (≋-trans (++⁺ ≋-refl eq₁) eq₂)
+      }
+    }
+  }
+
+∙-identityˡ : ∀ {a} → LeftIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
+∙-identityˡ X = record
+  { f = λ
+    { record { l₁ = [] ; l₂∈B = l∈X ; eq = eq } → X.∈-resp-≋ eq l∈X
+    }
+  ; f⁻¹ = λ l∈X → record
+    { l₁∈A = lift ≡.refl
+    ; l₂∈B = l∈X
+    ; eq = ≋-refl
+    }
+  }
+  where
+  module X = Language X
 
-∙-unique-prefix : ∀ {a b} (A : Language a) (B : Language b) → Empty (flast A ∩ first B) → ¬ (null A) → ∀ {l} → (l∈A∙B l∈A∙B′ : l ∈ A ∙ B) → proj₁ l∈A∙B ≋ proj₁ l∈A∙B′
-∙-unique-prefix _ _ _ ¬n₁ ([] , l₁∈A , _) _ = ⊥-elim (¬n₁ l₁∈A)
-∙-unique-prefix _ _ _ ¬n₁ (_ ∷ _ , _) ([] , l₁′∈A , _) = ⊥-elim (¬n₁ l₁′∈A)
-∙-unique-prefix A B ∄[l₁∩f₂] _ (c ∷ l₁ , l₁∈A , l₂ , l₂∈B , eq₁) (c′ ∷ l₁′ , l₁′∈A , l₂′ , l₂′∈B , eq₂) with compare (c ∷ l₁) l₂ (c′ ∷ l₁′) l₂′ (≋-trans eq₁ (≋-sym eq₂))
-... | cmp with <?> cmp
-... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] w ((-, (λ ()) , l₁′∈A , -, A.∈-resp-≋ eq₃ l₁∈A) , (-, B.∈-resp-≋ (≋-sym eq₄) l₂′∈B)))
+∙-unique-prefix : ∀ {a b} (A : Language a) (B : Language b) → Empty (flast A ∩ first B) → ¬ (null A) → ∀ {l} → (l∈A∙B l∈A∙B′ : l ∈ A ∙ B) → Concat.l₁ l∈A∙B ≋ Concat.l₁ l∈A∙B′ × Concat.l₂ l∈A∙B ≋ Concat.l₂ l∈A∙B′
+∙-unique-prefix A B ∄[l₁∩f₂] ¬n₁ l∈A∙B l∈A∙B′ with Compare.compare (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (Concat.l₁ l∈A∙B′) (Concat.l₂ l∈A∙B′) (≋-trans (Concat.eq l∈A∙B) (≋-sym (Concat.eq l∈A∙B′)))
+... | cmp with Compare.<?> cmp
+... | tri< l _ _ = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B′)}) , (Concat.l₁∈A l∈A∙B′) , -, A.∈-resp-≋ eq₃ (Concat.l₁∈A l∈A∙B)) , (-, B.∈-resp-≋ (≋-sym eq₄) (Concat.l₂∈B l∈A∙B′))))
   where
   module A = Language A
   module B = Language B
-  lsplit = left-split cmp l
+  lsplit = Compare.left-split cmp l
   w = proj₁ lsplit
   eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) lsplit
   eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) lsplit
-... | tri≈ _ e _ = eq-split cmp e
-... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] w ((-, (λ ()) , l₁∈A , -, A.∈-resp-≋ (≋-sym eq₃) l₁′∈A) , (-, (B.∈-resp-≋ eq₄ l₂∈B))))
+... | tri≈ _ e _ = Compare.eq-split cmp e
+... | tri> _ _ r = ⊥-elim (∄[l₁∩f₂] w ((-, (λ { ≡.refl → ¬n₁ (Concat.l₁∈A l∈A∙B)}) , (Concat.l₁∈A l∈A∙B) , -, A.∈-resp-≋ (≋-sym eq₃) (Concat.l₁∈A l∈A∙B′)) , (-, (B.∈-resp-≋ eq₄ (Concat.l₂∈B l∈A∙B)))))
   where
   module A = Language A
   module B = Language B
-  rsplit = right-split cmp r
+  rsplit = Compare.right-split cmp r
   w = proj₁ rsplit
   eq₃ = (proj₁ ∘ proj₂ ∘ proj₂) rsplit
   eq₄ = (proj₂ ∘ proj₂ ∘ proj₂) rsplit
+
+∙-identityʳ : ∀ {a} → RightIdentity _≈_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝) _∙_
+∙-identityʳ X = record
+  { f = λ
+    { record { l₁ = l₁ ; l₂ = [] ; l₁∈A = l∈X ; eq = eq } → X.∈-resp-≋ (≋-trans (≋-sym (≋-reflexive (++-identityʳ l₁))) eq) l∈X
+    }
+  ; f⁻¹ = λ {l} l∈X → record
+    { l₁∈A = l∈X
+    ; l₂∈B = lift ≡.refl
+    ; eq = ≋-reflexive (++-identityʳ l)
+    }
+  }
+  where
+  module X = Language X
+
+isMagma : ∀ {a} → IsMagma _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+isMagma {a} = record
+  { isEquivalence = ≈-isEquivalence
+  ; ∙-cong = ∙-cong {a}
+  }
+
+isSemigroup : ∀ {a} → IsSemigroup _≈_ (_∙_ {c ⊔ ℓ ⊔ a})
+isSemigroup {a} = record
+  { isMagma = isMagma {a}
+  ; assoc = ∙-assoc
+  }
+
+isMonoid : ∀ {a} → IsMonoid _≈_ _∙_ (𝕃.Lift (ℓ ⊔ a) ｛ε｝)
+isMonoid {a} = record
+  { isSemigroup = isSemigroup {a}
+  ; identity = ∙-identityˡ {a} , ∙-identityʳ {a}
+  }
diff --git a/src/Cfe/Type/Base.agda b/src/Cfe/Type/Base.agda
index 438dd65..33af9f6 100644
--- a/src/Cfe/Type/Base.agda
+++ b/src/Cfe/Type/Base.agda
@@ -10,6 +10,7 @@ open Setoid over using () renaming (Carrier to C; _≈_ to _∼_)
 
 open import Cfe.Language over hiding (_≤_; _≈_)
 open import Data.Bool as 𝔹 hiding (_∨_) renaming (_≤_ to _≤ᵇ_)
+open import Data.Empty.Polymorphic
 open import Level as L renaming (suc to lsuc)
 open import Relation.Unary as U
 open import Relation.Binary.PropositionalEquality using (_≡_)
@@ -45,8 +46,8 @@ _∨_ : ∀ {fℓ₁ lℓ₁ fℓ₂ lℓ₂} → Type fℓ₁ lℓ₁ → Type
 _∙_ : ∀ {fℓ₁ lℓ₁ fℓ₂ lℓ₂} → Type fℓ₁ lℓ₁ → Type fℓ₂ lℓ₂ → Type (fℓ₁ ⊔ fℓ₂) (lℓ₁ ⊔ fℓ₂ ⊔ lℓ₂)
 _∙_ {lℓ₁ = lℓ₁} {fℓ₂} {lℓ₂} τ₁ τ₂ = record
   { Null = Null τ₁ ∧ Null τ₂
-  ; First = First τ₁ ∪ (if Null τ₁ then First τ₂ else λ x → L.Lift fℓ₂ (x U.∈ U.∅))
-  ; Flast = Flast τ₂ ∪ (if Null τ₂ then First τ₂ ∪ Flast τ₁ else λ x → L.Lift (lℓ₁ ⊔ fℓ₂) (x U.∈ U.∅))
+  ; First = First τ₁ ∪ (if Null τ₁ then First τ₂ else λ x → ⊥)
+  ; Flast = Flast τ₂ ∪ (if Null τ₂ then First τ₂ ∪ Flast τ₁ else λ x → ⊥)
   }
 
 record _⊨_ {a} {fℓ} {lℓ} (A : Language a) (τ : Type fℓ lℓ) : Set (c ⊔ a ⊔ fℓ ⊔ lℓ) where
diff --git a/src/Cfe/Type/Properties.agda b/src/Cfe/Type/Properties.agda
index 37f491b..e9ed634 100644
--- a/src/Cfe/Type/Properties.agda
+++ b/src/Cfe/Type/Properties.agda
@@ -19,12 +19,15 @@ open import Data.Bool renaming (_≤_ to _≤ᵇ_; _∨_ to _∨ᵇ_)
 open import Data.Bool.Properties hiding (≤-reflexive; ≤-trans)
 open import Data.Empty
 open import Data.List hiding (null)
+open import Data.List.Properties using (++-identityʳ; ++-assoc)
 open import Data.List.Relation.Binary.Equality.Setoid over
 open import Data.Nat hiding (_≤ᵇ_; _^_) renaming (_≤_ to _≤ⁿ_)
 open import Data.Nat.Properties using (≤-stepsˡ; ≤-stepsʳ) renaming (≤-refl to ≤ⁿ-refl)
 open import Data.Product as Product
 open import Data.Sum as Sum
+import Level as L
 open import Function hiding (_⟶_)
+import Relation.Unary as U
 open import Relation.Unary.Properties
 open import Relation.Binary.PropositionalEquality
 
@@ -118,19 +121,81 @@ L⊨τε⇒L≤｛ε｝{L = L} L⊨τε = record
 ∙-⊨ : ∀ {a b fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} {B : Language b} {τ₁ : Type fℓ₁ lℓ₁} {τ₂ : Type fℓ₂ lℓ₂} →
       A ⊨ τ₁ → B ⊨ τ₂ → τ₁ ⊛ τ₂ → A ∙ˡ B ⊨ τ₁ ∙ τ₂
 ∙-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ τ₁⊛τ₂ = record
-  { n⇒n = λ { ([] , l∈A , _) → ⊥-elim (L⊨τ+¬N⇒ε∉L A⊨τ₁ τ₁⊛τ₂.¬n₁ l∈A) }
+  { n⇒n = λ { record { l₁ = [] ; l₁∈A = ε∈A } → ⊥-elim (L⊨τ+¬N⇒ε∉L A⊨τ₁ τ₁⊛τ₂.¬n₁ ε∈A) }
   ; f⇒f = λ
-    { (_ , [] , l∈A , l′ , l′∈B , _) → ⊥-elim (L⊨τ+¬N⇒ε∉L A⊨τ₁ τ₁⊛τ₂.¬n₁ l∈A)
-    ; (_ , x ∷ l , l∈A , l′ , l′∈B , x≈x ∷ _) → inj₁ (A⊨τ₁.f⇒f (l , A.∈-resp-≋ (x≈x ∷ ≋-refl) l∈A))
+    { (_ , record { l₁ = [] ; l₁∈A = ε∈A }) → ⊥-elim (L⊨τ+¬N⇒ε∉L A⊨τ₁ τ₁⊛τ₂.¬n₁ ε∈A)
+    ; (_ , record { l₁ = x ∷ l ; l₁∈A = xl∈A ; eq = x∼x ∷ _ }) → inj₁ (A⊨τ₁.f⇒f (l , A.∈-resp-≋ (x∼x ∷ ≋-refl) xl∈A))
     }
-  ; l⇒l = {!!}
+  ; l⇒l = l⇒l
   }
   where
   module A = Language A
+  module B = Language B
   module A⊨τ₁ = _⊨_ A⊨τ₁
   module B⊨τ₂ = _⊨_ B⊨τ₂
   module τ₁⊛τ₂ = _⊛_ τ₁⊛τ₂
 
+  null-case : ∀ {c} → null B → Flast τ₂ c ⊎ First τ₂ c ⊎ Flast τ₁ c → Flast (τ₁ ∙ τ₂) c
+  null-case {c} ε∈B proof = case ∃[ b ] (null B → T b) ∋ Null τ₂ , B⊨τ₂.n⇒n return (λ (b , _) → (Flast τ₂ U.∪ (if b then _ else _)) c) of λ
+    { (false , n⇒n) → ⊥-elim (n⇒n ε∈B)
+    ; (true , _) → proof
+    }
+
+  l⇒l : flast (A ∙ˡ B) U.⊆ Flast (τ₁ ∙ τ₂)
+  l⇒l {c} (l , l≢ε , l∈A∙B @ record {l₂ = l₂} , l′ , lcl′∈A∙B) with Compare.compare
+    (Concat.l₁ l∈A∙B)
+    (Concat.l₂ l∈A∙B ++ c ∷ l′)
+    (Concat.l₁ lcl′∈A∙B)
+    (Concat.l₂ lcl′∈A∙B)
+    (begin
+      Concat.l₁ l∈A∙B ++ Concat.l₂ l∈A∙B ++ c ∷ l′   ≡˘⟨ ++-assoc (Concat.l₁ l∈A∙B) (Concat.l₂ l∈A∙B) (c ∷ l′) ⟩
+      (Concat.l₁ l∈A∙B ++ Concat.l₂ l∈A∙B) ++ c ∷ l′ ≈⟨ ++⁺ (Concat.eq l∈A∙B) ≋-refl ⟩
+      l ++ c ∷ l′                                    ≈˘⟨ Concat.eq lcl′∈A∙B ⟩
+      Concat.l₁ lcl′∈A∙B ++ Concat.l₂ lcl′∈A∙B        ∎)
+    where
+    open import Relation.Binary.Reasoning.Setoid ≋-setoid
+  ... | cmp with Compare.<?> cmp
+  ... | tri< x _ _ = ⊥-elim (τ₁⊛τ₂.∄[l₁∩f₂] y (A⊨τ₁.l⇒l (-, l₁′≢ε , Concat.l₁∈A lcl′∈A∙B , -, l₁′yw∈A) , B⊨τ₂.f⇒f (-, yw′∈B)))
+    where
+    lsplit = Compare.left-split cmp x
+    y = proj₁ lsplit
+    l₁′≢ε = λ { refl → case ∃[ b ] T (not b) × (null A → T b) ∋ Null τ₁ , τ₁⊛τ₂.¬n₁ , A⊨τ₁.n⇒n of λ
+      { (false , _ , n⇒n) → n⇒n (Concat.l₁∈A lcl′∈A∙B)
+      ; (true , ¬n₁ , _) → ¬n₁
+      } }
+    l₁′yw∈A = A.∈-resp-≋ (proj₁ (proj₂ (proj₂ lsplit))) (Concat.l₁∈A l∈A∙B)
+    yw′∈B = B.∈-resp-≋ (≋-sym (proj₂ (proj₂ (proj₂ lsplit)))) (Concat.l₂∈B lcl′∈A∙B)
+  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = [] } , l′ , lcl′∈A∙B) | cmp | tri≈ _ x _ =
+    null-case (Concat.l₂∈B l∈A∙B) (inj₂ (inj₁ (B⊨τ₂.f⇒f (-, cl′∈B))))
+    where
+    esplit = Compare.eq-split cmp x
+    cl′∈B = B.∈-resp-≋ (≋-sym (proj₂ esplit)) (Concat.l₂∈B lcl′∈A∙B)
+  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = _ ∷ _ } , l′ , lcl′∈A∙B) | cmp | tri≈ _ x _ =
+    inj₁ (B⊨τ₂.l⇒l (-, (λ ()) , Concat.l₂∈B l∈A∙B , -, l₂cl′∈A∙B))
+    where
+    esplit = Compare.eq-split cmp x
+    l₂cl′∈A∙B = B.∈-resp-≋ (≋-sym (proj₂ esplit)) (Concat.l₂∈B lcl′∈A∙B)
+  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = [] } , l′ , lcl′∈A∙B) | cmp | tri> _ _ x =
+    null-case (Concat.l₂∈B l∈A∙B) (inj₂ (inj₂ (A⊨τ₁.l⇒l (-, l≢ε , l∈A , -, lcw∈A))))
+    where
+    rsplit = Compare.right-split cmp x
+    c∼y = case proj₂ (proj₂ (proj₂ rsplit)) of λ { (c∼y ∷ _) → c∼y }
+    l₁≋l = ≋-trans (≋-sym (≋-reflexive (++-identityʳ (Concat.l₁ l∈A∙B)))) (Concat.eq l∈A∙B)
+    lcw≋l₁yw = ≋-sym (≋-trans (++⁺ (≋-sym l₁≋l) (c∼y ∷ ≋-refl)) (proj₁ (proj₂ (proj₂ rsplit))))
+    l∈A = A.∈-resp-≋ l₁≋l (Concat.l₁∈A l∈A∙B)
+    lcw∈A = A.∈-resp-≋ lcw≋l₁yw (Concat.l₁∈A lcl′∈A∙B)
+  l⇒l {c} (l , l≢ε , l∈A∙B @ record { l₂ = y ∷ _ } , l′ , lcl′∈A∙B) | cmp | tri> _ _ x =
+    ⊥-elim (τ₁⊛τ₂.∄[l₁∩f₂] y (A⊨τ₁.l⇒l (-, l₁≢ε , Concat.l₁∈A l∈A∙B , -, l₁yw∈A) , B⊨τ₂.f⇒f (-, Concat.l₂∈B l∈A∙B)))
+    where
+    rsplit = Compare.right-split cmp x
+    l₁≢ε = λ { refl → case ∃[ b ] T (not b) × (null A → T b) ∋ Null τ₁ , τ₁⊛τ₂.¬n₁ , A⊨τ₁.n⇒n of λ
+      { (false , _ , n⇒n) → n⇒n (Concat.l₁∈A l∈A∙B)
+      ; (true , ¬n₁ , _) → ¬n₁
+      } }
+    y∼z = case proj₂ (proj₂ (proj₂ rsplit)) of λ { (y∼z ∷ _) → y∼z }
+    l₁′≋l₁yw = ≋-sym (≋-trans (++⁺ ≋-refl (y∼z ∷ ≋-refl)) (proj₁ (proj₂ (proj₂ rsplit))))
+    l₁yw∈A = A.∈-resp-≋ l₁′≋l₁yw (Concat.l₁∈A lcl′∈A∙B)
+
 ∪-⊨ : ∀ {a b fℓ₁ lℓ₁ fℓ₂ lℓ₂} {A : Language a} {B : Language b} {τ₁ : Type fℓ₁ lℓ₁} {τ₂ : Type fℓ₂ lℓ₂} →
       A ⊨ τ₁ → B ⊨ τ₂ → τ₁ # τ₂ → A ∪ B ⊨ τ₁ ∨ τ₂
 ∪-⊨ {A = A} {B} {τ₁} {τ₂} A⊨τ₁ B⊨τ₂ τ₁#τ₂ = record