------------------------------------------------------------------------
-- Lemmas related to expansion and CCS
------------------------------------------------------------------------

{-# OPTIONS --sized-types #-}

open import Prelude hiding (module W; step-→)

module Expansion.CCS {ℓ} {Name : Type ℓ} where

open import Equality.Propositional
open import Prelude.Size

open import Function-universe equality-with-J hiding (id; _∘_)

import Bisimilarity.CCS as SL
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
import Expansion.Equational-reasoning-instances
open import Labelled-transition-system.CCS Name
open import Relation

open import Bisimilarity CCS as S using (_∼_)
open import Bisimilarity.Weak CCS as W using (_≈_; force)
open import Expansion CCS
import Labelled-transition-system.Equational-reasoning-instances CCS
  as Dummy

-- Some lemmas used to prove the congruence lemmas below as well as
-- similar results in Bisimilarity.Weak.CCS.

module Cong-lemmas
  ({R} R′ : Proc ∞ → Proc ∞ → Type ℓ)
  ⦃ _ : Reflexive R′ ⦄
  ⦃ _ : Convertible R R′ ⦄
  ⦃ _ : Convertible R′ R′ ⦄
  ⦃ _ : Transitive′ R′ _∼_ ⦄
  ⦃ _ : Transitive _∼_ R′ ⦄
  {_[_]↝_ : Proc ∞ → Label → Proc ∞ → Type ℓ}
  (right-to-left :
   ∀ {P Q} → R P Q →
   ∀ {Q′ μ} → Q [ μ ]⟶ Q′ → ∃ λ P′ → P [ μ ]↝ P′ × R′ P′ Q′)
  ⦃ _ : ∀ {μ} → Convertible _[ μ ]↝_ _[ μ ]↝_ ⦄
  ⦃ _ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]↝_ ⦄
  (↝→[]⇒ : ∀ {P Q a} → P [ name a ]↝ Q → P [ name a ]⇒ Q)
  ([]⇒→↝ : ∀ {P Q} → P [ τ ]⇒ Q → P [ τ ]↝ Q)
  (map-↝ :
    {F : Proc ∞ → Proc ∞} →
    (∀ {P P′ μ} → P [ μ ]⟶ P′ → F P [ μ ]⟶ F P′) →
    ∀ {P P′ μ} → P [ μ ]↝ P′ → F P [ μ ]↝ F P′)
  (map-↝′ :
    ∀ {μ} {F : Proc ∞ → Proc ∞} →
    (∀ {P P′ μ} → Silent μ → P [ μ ]⟶ P′ → F P [ μ ]⟶ F P′) →
    (∀ {P P′} → P [ μ ]⟶ P′ → F P [ μ ]⟶ F P′) →
    ∀ {P P′} → P [ μ ]↝ P′ → F P [ μ ]↝ F P′)
  (zip-↝ :
    {F : Proc ∞ → Proc ∞ → Proc ∞} →
    (∀ {P P′ Q μ} → P [ μ ]⟶ P′ → F P Q [ μ ]⟶ F P′ Q) →
    (∀ {P Q Q′ μ} → Q [ μ ]⟶ Q′ → F P Q [ μ ]⟶ F P Q′) →
    ∀ {μ₁ μ₂ μ₃} →
    (Silent μ₁ → Silent μ₂ → Silent μ₃) →
    (∀ {P P′ Q} → P [ μ₁ ]⟶ P′ → Silent μ₂ → F P Q [ μ₃ ]⟶ F P′ Q) →
    (∀ {P Q Q′} → Silent μ₁ → Q [ μ₂ ]⟶ Q′ → F P Q [ μ₃ ]⟶ F P Q′) →
    (∀ {P P′ Q Q′} →
     P [ μ₁ ]⟶ P′ → Q [ μ₂ ]⟶ Q′ → F P Q [ μ₃ ]⟶ F P′ Q′) →
    ∀ {P P′ Q Q′} →
    P [ μ₁ ]↝ P′ → Q [ μ₂ ]↝ Q′ → F P Q [ μ₃ ]↝ F P′ Q′)
  (!-lemma :
    (∀ {P Q μ} → P [ μ ]⇒ Q → ! P [ μ ]⇒ ! P ∣ Q) →
    ∀ {P Q μ} → P [ μ ]↝ Q →
    ∃ λ P′ → ((! P) [ μ ]↝ P′) × P′ ∼ ! P ∣ Q)
  where

  private

    infix -3 rl-result-↝

    rl-result-↝ : ∀ {P P′ Q′} μ → P [ μ ]↝ P′ → R′ P′ Q′ →
                  ∃ λ P′ → (P [ μ ]↝ P′) × R′ P′ Q′
    rl-result-↝ _ P↝P′ P′≳′Q′ = _ , P↝P′ , P′≳′Q′

    syntax rl-result-↝ μ P↝P′ P′≳′Q′ = P↝P′ ↝[ μ ] P′≳′Q′

  ∣-cong :
    (∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
    ∀ {P₁ P₂ Q₁ Q₂ R₂ μ} →
    R P₁ P₂ → R Q₁ Q₂ → P₂ ∣ Q₂ [ μ ]⟶ R₂ →
    ∃ λ R₁ → ((P₁ ∣ Q₁) [ μ ]↝ R₁) × R′ R₁ R₂
  ∣-cong _∣-cong′_ P₁≳P₂ Q₁≳Q₂ = λ where
    (par-left  tr)  → Σ-map (_∣ _)
                        (Σ-map (map-↝ par-left)
                               (_∣-cong′ convert Q₁≳Q₂))
                        (right-to-left P₁≳P₂ tr)
    (par-right tr)  → Σ-map (_ ∣_)
                        (Σ-map (map-↝ par-right)
                               (convert P₁≳P₂ ∣-cong′_))
                        (right-to-left Q₁≳Q₂ tr)
    (par-τ tr₁ tr₂) → Σ-zip _∣_
                        (Σ-zip (zip-↝ par-left par-right
                                      (λ ()) (λ _ ()) (λ ())
                                      par-τ)
                               _∣-cong′_)
                        (right-to-left P₁≳P₂ tr₁)
                        (right-to-left Q₁≳Q₂ tr₂)

  ·-cong :
    ∀ {P₁ P₂ Q₂ μ μ′} →
    R′ (force P₁) (force P₂) → μ · P₂ [ μ′ ]⟶ Q₂ →
    ∃ λ Q₁ → ((μ · P₁) [ μ′ ]↝ Q₁) × R′ Q₁ Q₂
  ·-cong P₁≳P₂ action = _ , convert (⟶: action) , P₁≳P₂

  ⟨ν⟩-cong :
    (∀ {a P P′} → R′ P P′ → R′ (⟨ν a ⟩ P) (⟨ν a ⟩ P′)) →
    ∀ {a μ P P′ Q′} →
    R P P′ → ⟨ν a ⟩ P′ [ μ ]⟶ Q′ →
    ∃ λ Q → (⟨ν a ⟩ P [ μ ]↝ Q) × R′ Q Q′
  ⟨ν⟩-cong ⟨ν⟩-cong′ {a} {μ} {P} P≳P′
           (restriction {P′ = Q′} a∉μ P′⟶Q′) =
    case right-to-left P≳P′ P′⟶Q′ of λ where
      (Q , P↝Q , Q≳′Q′) →
        ⟨ν a ⟩ P   →⟨ map-↝′ (restriction ∘ ∉τ) (restriction a∉μ) P↝Q ⟩■
          ↝[ μ ]
        ⟨ν a ⟩ Q   ∼⟨ ⟨ν⟩-cong′ Q≳′Q′ ⟩■
        ⟨ν a ⟩ Q′

  !-cong-lemma₁ : ∀ {P Q μ} → P [ μ ]⇒ Q → ! P [ μ ]⇒ ! P ∣ Q
  !-cong-lemma₁ {P} {Q} {μ} = λ where
    (steps {q′ = Q′} done P⟶Q′ Q′⇒Q) →
      ! P       [ μ ]⇒⟨ replication (par-right P⟶Q′) ⟩
      ! P ∣ Q′  →⟨ map-⇒ par-right Q′⇒Q ⟩■
      ! P ∣ Q

    (steps {p′ = P″} {q′ = Q′}
           (step {q = P′} {μ = μ′} μ′s P⟶P′ P′⇒P″)
           P″⟶Q′ Q′⇒Q) →
      ! P       →⟨ ⟶→⇒ μ′s (replication (par-right P⟶P′)) ⟩
      ! P ∣ P′  →⟨ map-⇒ par-right P′⇒P″ ⟩
      ! P ∣ P″  [ μ ]⇒⟨ par-right P″⟶Q′ ⟩
      ! P ∣ Q′  →⟨ map-⇒ par-right Q′⇒Q ⟩■
      ! P ∣ Q

  !-cong-lemma₂ :
    ∀ {P Q₁ Q₂ a} →
    P [ name a ]⇒ Q₁ → P [ name (co a) ]⇒ Q₂ →
    ∃ λ R → ! P [ τ ]⇒ R × R ∼ (! P ∣ Q₁) ∣ Q₂
  !-cong-lemma₂ {P} {Q₁} {Q₂} {a} = λ where
    (steps {q′ = Q₁′} done P⟶Q₁′ Q₁′⇒Q₁)
      (steps {q′ = Q₂′} done P⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                [ τ ]⇒⟨ replication (par-τ (replication (par-right P⟶Q₁′)) P⟶Q₂′) ⟩
         (! P ∣ Q₁′) ∣ Q₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₁′⇒Q₁) Q₂′⇒Q₂ ⟩■
         (! P ∣ Q₁) ∣ Q₂)
      , reflexive

    (steps {q′ = Q₁′} done P⟶Q₁′ Q₁′⇒Q₁)
      (steps {p′ = P₂″} {q′ = Q₂′}
             (step {q = P₂′} {μ = μ} μs P⟶P₂′ P₂′⇒P₂″)
             P₂″⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                →⟨ ⟶→⇒ μs (replication (par-right P⟶P₂′)) ⟩
         ! P ∣ P₂′          →⟨ map-⇒ par-right P₂′⇒P₂″ ⟩
         ! P ∣ P₂″          [ τ ]⇒⟨ par-τ (replication (par-right P⟶Q₁′)) P₂″⟶Q₂′ ⟩
         (! P ∣ Q₁′) ∣ Q₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₁′⇒Q₁) Q₂′⇒Q₂ ⟩■
         (! P ∣ Q₁) ∣ Q₂)
      , reflexive

    (steps {p′ = P₁″} {q′ = Q₁′}
           (step {q = P₁′} {μ = μ} μs P⟶P₁′ P₁′⇒P₁″)
           P₁″⟶Q₁′ Q₁′⇒Q₁)
      (steps {q′ = Q₂′} done P⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                →⟨ ⟶→⇒ μs (replication (par-right P⟶P₁′)) ⟩
         ! P ∣ P₁′          →⟨ map-⇒ par-right P₁′⇒P₁″ ⟩
         ! P ∣ P₁″          [ τ ]⇒⟨ par-τ′ (sym $ co-involutive a) (replication (par-right P⟶Q₂′)) P₁″⟶Q₁′ ⟩
         (! P ∣ Q₂′) ∣ Q₁′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₂′⇒Q₂) Q₁′⇒Q₁ ⟩■
         (! P ∣ Q₂) ∣ Q₁)
      , ((! P ∣ Q₂) ∣ Q₁  ∼⟨ SL.swap-rightmost ⟩■
         (! P ∣ Q₁) ∣ Q₂)

    (steps {p′ = P₁″} {q′ = Q₁′}
           (step {q = P₁′} {μ = μ₁} μ₁s P⟶P₁′ P₁′⇒P₁″)
           P₁″⟶Q₁′ Q₁′⇒Q₁)
      (steps {p′ = P₂″} {q′ = Q₂′}
             (step {q = P₂′} {μ = μ₂} μ₂s P⟶P₂′ P₂′⇒P₂″)
             P₂″⟶Q₂′ Q₂′⇒Q₂) →
        _
      , (! P                →⟨ ⟶→⇒ μ₂s (replication (par-right P⟶P₂′)) ⟩
         ! P ∣ P₂′          →⟨ ⟶→⇒ μ₁s (par-left (replication (par-right P⟶P₁′))) ⟩
         (! P ∣ P₁′) ∣ P₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right P₁′⇒P₁″) P₂′⇒P₂″ ⟩
         (! P ∣ P₁″) ∣ P₂″  [ τ ]⇒⟨ par-τ (par-right P₁″⟶Q₁′) P₂″⟶Q₂′ ⟩
         (! P ∣ Q₁′) ∣ Q₂′  →⟨ zip-⇒ par-left par-right (map-⇒ par-right Q₁′⇒Q₁) Q₂′⇒Q₂ ⟩■
         (! P ∣ Q₁) ∣ Q₂)
      , reflexive

  !-cong :
    (∀ {P P′ Q Q′} → R′ P P′ → R′ Q Q′ → R′ (P ∣ Q) (P′ ∣ Q′)) →
    (∀ {P P′} → R′ P P′ → R′ (! P) (! P′)) →
    ∀ {P P′ Q′ μ} →
    R P P′ → ! P′ [ μ ]⟶ Q′ →
    ∃ λ Q → ((! P) [ μ ]↝ Q) × R′ Q Q′
  !-cong _∣-cong′_ !-cong′_ {P} {P′} {Q′} {μ} P≳P′ !P′⟶Q′ =
    case SL.6-1-3-2 !P′⟶Q′ of λ where

      (inj₁ (P″ , P′⟶P″ , Q′∼!P′∣P″)) →
        let Q , P↝Q  , Q≳′P″  = right-to-left P≳P′ P′⟶P″
            R , !P↝R , R∼!P∣Q = !-lemma !-cong-lemma₁ P↝Q
        in
          ! P        →⟨ !P↝R ⟩■
            ↝[ μ ]
          R          ∼⟨ R∼!P∣Q ⟩
          ! P ∣ Q    ∼′⟨ (!-cong′ (convert P≳P′)) ∣-cong′ Q≳′P″ ⟩
          ! P′ ∣ P″  ∼⟨ symmetric Q′∼!P′∣P″ ⟩■
          Q′

      (inj₂ (refl , P″ , P‴ , a , P′⟶P″ , P′⟶P‴ , Q′∼!P′∣P″∣P‴)) →
        let Q₁ , P↝Q₁ , Q₁≳′P″ = right-to-left P≳P′ P′⟶P″
            Q₂ , P↝Q₂ , Q₂≳′P‴ = right-to-left P≳P′ P′⟶P‴

            R , !P⇒R , R∼[!P∣Q₁]∣Q₂ =
              !-cong-lemma₂ (↝→[]⇒ P↝Q₁) (↝→[]⇒ P↝Q₂)
        in
          ! P               →⟨ []⇒→↝ !P⇒R ⟩■
            ↝[ τ ]
          R                 ∼⟨ R∼[!P∣Q₁]∣Q₂ ⟩
          (! P ∣ Q₁) ∣ Q₂   ∼′⟨ ((!-cong′ (convert P≳P′)) ∣-cong′ Q₁≳′P″) ∣-cong′ Q₂≳′P‴ ⟩
          (! P′ ∣ P″) ∣ P‴  ∼⟨ symmetric Q′∼!P′∣P″∣P‴ ⟩■
          Q′

  ⊕·-cong :
    ∀ {P Q Q′ S′ μ μ′} →
    R′ (force Q) (force Q′) → P ⊕ μ · Q′ [ μ′ ]⟶ S′ →
    ∃ λ S → ((P ⊕ μ · Q) [ μ′ ]↝ S) × R′ S S′
  ⊕·-cong {P} {Q} {Q′} {S′} {μ} {μ′} Q≳Q′ = λ where
    (sum-left P⟶S′) →
      P ⊕ μ · Q  →⟨ ⟶: sum-left P⟶S′ ⟩■
        ↝[ μ′ ]
      S′         ■

    (sum-right action) →
      P ⊕ μ · Q  →⟨ ⟶: sum-right action ⟩■
        ↝[ μ ]
      force Q    ∼⟨ Q≳Q′ ⟩■
      force Q′

  ·⊕·-cong :
    ∀ {μ₁ μ₂ P₁ P₁′ P₂ P₂′ S′ μ} →
    R′ (force P₁) (force P₁′) → R′ (force P₂) (force P₂′) →
    μ₁ · P₁′ ⊕ μ₂ · P₂′ [ μ ]⟶ S′ →
    ∃ λ S → ((μ₁ · P₁ ⊕ μ₂ · P₂) [ μ ]↝ S) × R′ S S′
  ·⊕·-cong {μ₁} {μ₂} {P₁} {P₁′} {P₂} {P₂′} P₁≳P₁′ P₂≳P₂′ = λ where
    (sum-left action) →
      μ₁ · P₁ ⊕ μ₂ · P₂  →⟨ ⟶: sum-left action ⟩■
        ↝[ μ₁ ]
      force P₁           ∼⟨ P₁≳P₁′ ⟩■
      force P₁′

    (sum-right action) →
      μ₁ · P₁ ⊕ μ₂ · P₂  →⟨ ⟶: sum-right action ⟩■
        ↝[ μ₂ ]
      force P₂           ∼⟨ P₂≳P₂′ ⟩■
      force P₂′

private
  module CL {i} =
    Cong-lemmas
      [ i ]_≳′_ right-to-left id id
      map-[]⇒ map-[]⇒′ (λ f g _ _ _ → zip-[]⇒ f g)
      (λ hyp P⇒Q → _ , hyp P⇒Q , reflexive)

mutual

  -- _∣_ preserves the expansion relation.

  infix  _∣-cong_ _∣-cong′_

  _∣-cong_ : ∀ {i P P′ Q Q′} →
             [ i ] P ≳ P′ → [ i ] Q ≳ Q′ → [ i ] P ∣ Q ≳ P′ ∣ Q′
  _∣-cong_ {i} P≳P′ Q≳Q′ =
    ⟨ lr P≳P′ Q≳Q′
    , CL.∣-cong _∣-cong′_ P≳P′ Q≳Q′
    ⟩
    where
    lr : ∀ {P P′ Q Q′ R μ} →
         [ i ] P ≳ P′ → [ i ] Q ≳ Q′ → P ∣ Q [ μ ]⟶ R →
         ∃ λ R′ → P′ ∣ Q′ [ μ ]⟶̂ R′ × [ i ] R ≳′ R′
    lr P≳P′ Q≳Q′ (par-left  tr)  = Σ-map (_∣ _)
                                         (Σ-map (map-⟶̂ par-left)
                                                (_∣-cong′ convert {a = ℓ} Q≳Q′))
                                     (left-to-right P≳P′ tr)
    lr P≳P′ Q≳Q′ (par-right tr)  = Σ-map (_ ∣_)
                                         (Σ-map (map-⟶̂ par-right)
                                                (convert {a = ℓ} P≳P′ ∣-cong′_))
                                     (left-to-right Q≳Q′ tr)
    lr P≳P′ Q≳Q′ (par-τ tr₁ tr₂) = Σ-zip _∣_
                                         (Σ-zip (zip-⟶̂ (λ ()) (λ _ ())
                                                       (λ ()) par-τ)
                                                _∣-cong′_)
                                     (left-to-right P≳P′ tr₁)
                                     (left-to-right Q≳Q′ tr₂)

  _∣-cong′_ : ∀ {i P P′ Q Q′} →
              [ i ] P ≳′ P′ → [ i ] Q ≳′ Q′ → [ i ] P ∣ Q ≳′ P′ ∣ Q′
  force (P≳P′ ∣-cong′ Q≳Q′) = force P≳P′ ∣-cong force Q≳Q′

-- _·_ preserves the expansion relation.

infix  _·-cong_ _·-cong′_

_·-cong_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≳′ force P′ → [ i ] μ · P ≳ μ′ · P′
_·-cong_ {i} {μ} {P = P} {P′} refl P≳P′ = ⟨ lr , CL.·-cong P≳P′ ⟩
  where
  lr : ∀ {Q μ″} →
       μ · P [ μ″ ]⟶ Q →
       ∃ λ Q′ → μ · P′ [ μ″ ]⟶̂ Q′ × [ i ] Q ≳′ Q′
  lr action = _ , ⟶→⟶̂ action , P≳P′

_·-cong′_ :
  ∀ {i μ μ′ P P′} →
  μ ≡ μ′ → [ i ] force P ≳′ force P′ → [ i ] μ · P ≳′ μ′ · P′
force (μ≡μ′ ·-cong′ P≳P′) = μ≡μ′ ·-cong P≳P′

-- _∙_ preserves the expansion relation.

infix  _∙-cong_ _∙-cong′_

_∙-cong_ : ∀ {i μ μ′ P P′} →
           μ ≡ μ′ → [ i ] P ≳ P′ → [ i ] μ ∙ P ≳ μ′ ∙ P′
refl ∙-cong P≳P′ = refl ·-cong convert {a = ℓ} P≳P′

_∙-cong′_ : ∀ {i μ μ′ P P′} →
            μ ≡ μ′ → [ i ] P ≳′ P′ → [ i ] μ ∙ P ≳′ μ′ ∙ P′
force (μ≡μ′ ∙-cong′ P≳P′) = μ≡μ′ ∙-cong force P≳P′

-- _∙ turns equal actions into processes related by the expansion
-- relation.

infix  _∙-cong _∙-cong′

_∙-cong : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≳ μ′ ∙
refl ∙-cong = reflexive

_∙-cong′ : ∀ {μ μ′} → μ ≡ μ′ → μ ∙ ≳′ μ′ ∙
refl ∙-cong′ = reflexive

mutual

  -- ⟨ν_⟩ preserves the expansion relation.

  ⟨ν_⟩-cong : ∀ {i a a′ P P′} →
              a ≡ a′ → [ i ] P ≳ P′ → [ i ] ⟨ν a ⟩ P ≳ ⟨ν a′ ⟩ P′
  ⟨ν_⟩-cong {i} {a} {P = P} {P′} refl P≳P′ =
    ⟨ lr
    , CL.⟨ν⟩-cong ⟨ν refl ⟩-cong′ P≳P′
    ⟩
    where
    lr : ∀ {Q μ} →
         ⟨ν a ⟩ P [ μ ]⟶ Q →
         ∃ λ Q′ → ⟨ν a ⟩ P′ [ μ ]⟶̂ Q′ × [ i ] Q ≳′ Q′
    lr {μ = μ} (restriction {P′ = Q} a∉μ P⟶Q)
      with left-to-right P≳P′ P⟶Q
    ... | Q′ , step P′⟶Q′ , Q≳′Q′ =
      ⟨ν a ⟩ Q   ∼⟨ ⟨ν refl ⟩-cong′ Q≳′Q′ ⟩■
      ⟨ν a ⟩ Q′
        ⟵̂[ μ ]   ←⟨ ⟶: restriction a∉μ P′⟶Q′ ⟩■
      ⟨ν a ⟩ P′

    ... | _ , done μs , Q≳′P′ =
      ⟨ν a ⟩ Q   ∼⟨ ⟨ν refl ⟩-cong′ Q≳′P′ ⟩■
      ⟨ν a ⟩ P′
        ⟵̂[ μ ]   ←⟨ ⟶̂: done μs ⟩■
      ⟨ν a ⟩ P′

  ⟨ν_⟩-cong′ : ∀ {i a a′ P P′} →
               a ≡ a′ → [ i ] P ≳′ P′ → [ i ] ⟨ν a ⟩ P ≳′ ⟨ν a′ ⟩ P′
  force (⟨ν a≡a′ ⟩-cong′ P≳P′) = ⟨ν a≡a′ ⟩-cong (force P≳P′)

mutual

  -- !_ preserves the expansion relation.

  infix  !-cong_ !-cong′_

  !-cong_ : ∀ {i P P′} →
            [ i ] P ≳ P′ → [ i ] ! P ≳ ! P′
  !-cong_ {i} {P} {P′} P≳P′ =
    ⟨ lr
    , CL.!-cong _∣-cong′_ !-cong′_ P≳P′
    ⟩
    where
    lr : ∀ {Q μ} →
         ! P [ μ ]⟶ Q →
         ∃ λ Q′ → ! P′ [ μ ]⟶̂ Q′ × [ i ] Q ≳′ Q′
    lr {Q} {μ} !P⟶Q = case SL.6-1-3-2 !P⟶Q of λ where

      (inj₁ (P″ , P⟶P″ , Q∼!P∣P″)) → case left-to-right P≳P′ P⟶P″ of λ where
        (_ , done s , P″≳′P′) → case silent≡τ s of λ where
          refl →
              _
            , (! P′  ■)
            , (Q          ∼⟨ Q∼!P∣P″ ⟩
               ! P  ∣ P″  ∼′⟨ !-cong′ (convert {a = ℓ} P≳P′) ∣-cong′ P″≳′P′ ⟩ S.∼:
               ! P′ ∣ P′  ∼⟨ SL.6-1-2 ⟩■
               ! P′)

        (Q′ , step P′⟶Q′ , P″≳′Q′) →
            _
          , (! P′ ∣ Q′  ←⟨ ⟶: replication (par-right P′⟶Q′) ⟩■
             ! P′)
          , (Q          ∼⟨ Q∼!P∣P″ ⟩
             ! P  ∣ P″  ∼⟨ !-cong′ (convert {a = ℓ} P≳P′) ∣-cong′ P″≳′Q′ ⟩■
             ! P′ ∣ Q′)

      (inj₂ (refl , P″ , P‴ , a , P⟶P″ , P⟶P‴ , Q≳!P∣P″∣P‴)) →
        case left-to-right P≳P′ P⟶P″ ,′
             left-to-right P≳P′ P⟶P‴ of λ where
          ((Q′ , step P′⟶Q′ , P″≳′Q′) ,
           (Q″ , step P′⟶Q″ , P‴≳′Q″)) →
              _
            , ((! P′ ∣ Q′) ∣ Q″  ←⟨ ⟶: replication (par-τ (replication (par-right P′⟶Q′)) P′⟶Q″) ⟩■
               ! P′)
            , (Q                 ∼⟨ Q≳!P∣P″∣P‴ ⟩
               (! P ∣ P″) ∣ P‴   ∼⟨ (!-cong′ (convert {a = ℓ} P≳P′) ∣-cong′ P″≳′Q′) ∣-cong′ P‴≳′Q″ ⟩■
               (! P′ ∣ Q′) ∣ Q″)

          ((_ , done () , _) , _)
          (_ , (_ , done () , _))

  !-cong′_ : ∀ {i P P′} → [ i ] P ≳′ P′ → [ i ] ! P ≳′ ! P′
  force (!-cong′ P≳P′) = !-cong (force P≳P′)

-- It is not necessarily the case that, if P expands P′, then P ⊕ Q is
-- weakly bisimilar to P′ ⊕ Q (assuming that Name is inhabited).
--
-- I based the counterexample on one in "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

¬⊕-congˡ-≳≈ : Name → ¬ (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)
¬⊕-congˡ-≳≈ x =
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)  ↝⟨ _$ τa≳a ⟩
  τ ∙ (a ∙) ⊕ b ∙ ≈ a ∙ ⊕ b ∙             ↝⟨ τa⊕b≉a⊕b ⟩□
  ⊥                                       □
  where
  a = x , true
  b = x , false

  τa≳a : ∀ {a} → τ ∙ (a ∙) ≳ a ∙
  τa≳a {a} =
    ⟨ (λ where
        action →
          a ∙       ■
            ⟵̂[ τ ]
          a ∙       ■)
    , (λ where
        action →
          τ ∙ (a ∙)      →⟨ ⟶: action ⟩
          a ∙            →⟨ ⟶: action ⟩■
            ⇒[ name a ]
          ∅              ■)
    ⟩

  τa⊕b≉a⊕b : ¬ τ ∙ (a ∙) ⊕ b ∙ ≈ a ∙ ⊕ b ∙
  τa⊕b≉a⊕b τa⊕b≈a⊕b
    with W.left-to-right τa⊕b≈a⊕b (sum-left action)
  ... | _ , non-silent ¬s _ , _ = ⊥-elim (¬s _)
  ... | _ , silent _ (step () (sum-left  action) _) , _
  ... | _ , silent _ (step () (sum-right action) _) , _
  ... | _ , silent _ done , a≈′a⊕b
    with W.right-to-left (force a≈′a⊕b) (sum-right action)
  ...   | _ , silent () _ , _
  ...   | _ , non-silent _ (steps done () _) , _
  ...   | _ , non-silent _ (steps (step () action _) _ _) , _

-- It is not necessarily the case that, if Q expands Q′, then P ⊕ Q is
-- weakly bisimilar to P ⊕ Q′ (assuming that Name is inhabited).

¬⊕-congʳ-≳≈ : Name → ¬ (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≈ P ⊕ Q′)
¬⊕-congʳ-≳≈ x ⊕-congʳ-≳≈ = ¬⊕-congˡ-≳≈ x ⊕-congˡ-≳≈
  where
  ⊕-congˡ-≳≈ : ∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q
  ⊕-congˡ-≳≈ {P} {P′} {Q} P≳P′ =
    P ⊕ Q   ∼⟨ SL.⊕-comm ⟩
    Q ⊕ P   ∼′⟨ ⊕-congʳ-≳≈ P≳P′ ⟩ S.∼:
    Q ⊕ P′  ∼⟨ SL.⊕-comm ⟩■
    P′ ⊕ Q

-- _⊕_ does not, in general, preserve the expansion relation in its
-- first argument (assuming that Name is inhabited).

¬⊕-congˡ : Name → ¬ (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≳ P′ ⊕ Q)
¬⊕-congˡ x =
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≳ P′ ⊕ Q)  ↝⟨ W.≳⇒≈ ∘_ ⟩
  (∀ {P P′ Q} → P ≳ P′ → P ⊕ Q ≈ P′ ⊕ Q)  ↝⟨ ¬⊕-congˡ-≳≈ x ⟩□
  ⊥                                       □

-- _⊕_ does not, in general, preserve the expansion relation in its
-- second argument (assuming that Name is inhabited).

¬⊕-congʳ : Name → ¬ (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≳ P ⊕ Q′)
¬⊕-congʳ x =
  (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≳ P ⊕ Q′)  ↝⟨ W.≳⇒≈ ∘_ ⟩
  (∀ {P Q Q′} → Q ≳ Q′ → P ⊕ Q ≈ P ⊕ Q′)  ↝⟨ ¬⊕-congʳ-≳≈ x ⟩□
  ⊥                                       □

-- Some congruence lemmas for combinations of _⊕_ and _·_.

⊕·-cong : ∀ {i P μ Q Q′} →
          [ i ] force Q ≳′ force Q′ → [ i ] P ⊕ μ · Q ≳ P ⊕ μ · Q′
⊕·-cong {i} {P} {μ} {Q} {Q′} Q≳Q′ =
  ⟨ lr , CL.⊕·-cong Q≳Q′ ⟩
  where
  lr : ∀ {R μ′} →
       P ⊕ μ · Q [ μ′ ]⟶ R →
       ∃ λ R′ → P ⊕ μ · Q′ [ μ′ ]⟶̂ R′ × [ i ] R ≳′ R′
  lr {R} {μ′} = λ where
    (sum-left P⟶R) →
      R           ■
        ⟵̂[ μ′ ]   ←⟨ ⟶: sum-left P⟶R ⟩■
      P ⊕ μ · Q′

    (sum-right action) →
      force Q     ∼⟨ Q≳Q′ ⟩■
      force Q′
        ⟵̂[ μ ]    ←⟨ ⟶: sum-right action ⟩■
      P ⊕ μ · Q′

⊕·-cong′ : ∀ {i P μ Q Q′} →
           [ i ] force Q ≳′ force Q′ → [ i ] P ⊕ μ · Q ≳′ P ⊕ μ · Q′
force (⊕·-cong′ Q≳Q′) = ⊕·-cong Q≳Q′

·⊕-cong : ∀ {i P P′ μ Q} →
          [ i ] force P ≳′ force P′ → [ i ] μ · P ⊕ Q ≳ μ · P′ ⊕ Q
·⊕-cong {P = P} {P′} {μ} {Q} P≳P′ =
  μ · P ⊕ Q   ∼⟨ SL.⊕-comm ⟩
  Q ⊕ μ · P   ∼′⟨ ⊕·-cong P≳P′ ⟩ S.∼:
  Q ⊕ μ · P′  ∼⟨ SL.⊕-comm ⟩■
  μ · P′ ⊕ Q

·⊕-cong′ : ∀ {i P P′ μ Q} →
           [ i ] force P ≳′ force P′ → [ i ] μ · P ⊕ Q ≳′ μ · P′ ⊕ Q
force (·⊕-cong′ P≳P′) = ·⊕-cong P≳P′

infix  _·⊕·-cong_ _·⊕·-cong′_

_·⊕·-cong_ :
  ∀ {i μ₁ μ₂ P₁ P₁′ P₂ P₂′} →
  [ i ] force P₁ ≳′ force P₁′ → [ i ] force P₂ ≳′ force P₂′ →
  [ i ] μ₁ · P₁ ⊕ μ₂ · P₂ ≳ μ₁ · P₁′ ⊕ μ₂ · P₂′
_·⊕·-cong_ {i} {μ₁} {μ₂} {P₁} {P₁′} {P₂} {P₂′} P₁≳P₁′ P₂≳P₂′ =
  ⟨ lr , CL.·⊕·-cong P₁≳P₁′ P₂≳P₂′ ⟩
  where
  lr : ∀ {R μ} → μ₁ · P₁ ⊕ μ₂ · P₂ [ μ ]⟶ R →
       ∃ λ R′ → μ₁ · P₁′ ⊕ μ₂ · P₂′ [ μ ]⟶̂ R′ × [ i ] R ≳′ R′
  lr = λ where
    (sum-left action) →
      force P₁             ∼⟨ P₁≳P₁′ ⟩■
      force P₁′
        ⟵̂[ μ₁ ]            ←⟨ ⟶: sum-left action ⟩■
      μ₁ · P₁′ ⊕ μ₂ · P₂′

    (sum-right action) →
      force P₂             ∼⟨ P₂≳P₂′ ⟩■
      force P₂′
        ⟵̂[ μ₂ ]            ←⟨ ⟶: sum-right action ⟩■
      μ₁ · P₁′ ⊕ μ₂ · P₂′

_·⊕·-cong′_ :
  ∀ {i μ₁ μ₂ P₁ P₁′ P₂ P₂′} →
  [ i ] force P₁ ≳′ force P₁′ → [ i ] force P₂ ≳′ force P₂′ →
  [ i ] μ₁ · P₁ ⊕ μ₂ · P₂ ≳′ μ₁ · P₁′ ⊕ μ₂ · P₂′
force (P₁≳′P₁′ ·⊕·-cong′ P₂≳′P₂′) = P₁≳′P₁′ ·⊕·-cong P₂≳′P₂′

-- _[_] preserves the expansion relation for non-degenerate contexts.
-- (This result is related to Theorem 6.5.25 in "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.)

infix  _[_]-cong _[_]-cong′

_[_]-cong :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≳ Qs x) →
  [ i ] C [ Ps ] ≳ C [ Qs ]
hole     [ Ps≳Qs ]-cong = Ps≳Qs _
∅        [ Ps≳Qs ]-cong = reflexive
D₁ ∣ D₂  [ Ps≳Qs ]-cong = (D₁ [ Ps≳Qs ]-cong) ∣-cong (D₂ [ Ps≳Qs ]-cong)
action D [ Ps≳Qs ]-cong = refl ·-cong λ { .force → force D [ Ps≳Qs ]-cong }
⟨ν⟩ D    [ Ps≳Qs ]-cong = ⟨ν refl ⟩-cong (D [ Ps≳Qs ]-cong)
! D      [ Ps≳Qs ]-cong = !-cong (D [ Ps≳Qs ]-cong)
D₁ ⊕ D₂  [ Ps≳Qs ]-cong = ⊕-cong Ps≳Qs D₁ D₂
  where
  _[_]-cong′ :
    ∀ {i n Ps Qs} {C : Context ∞ n} →
    Non-degenerate′ ∞ C → (∀ x → [ i ] Ps x ≳ Qs x) →
    [ i ] C [ Ps ] ≳′ C [ Qs ]
  force (D [ Ps≳Qs ]-cong′) = force D [ Ps≳Qs ]-cong

  ⊕-cong :
    ∀ {i n Ps Qs} {C₁ C₂ : Context ∞ n} →
    (∀ x → [ i ] Ps x ≳ Qs x) →
    Non-degenerate-summand ∞ C₁ →
    Non-degenerate-summand ∞ C₂ →
    [ i ] (C₁ [ Ps ]) ⊕ (C₂ [ Ps ]) ≳ (C₁ [ Qs ]) ⊕ (C₂ [ Qs ])
  ⊕-cong {Ps = Ps} {Qs} Ps≳Qs = λ where
    (process P₁) (process P₂) →
      (context P₁ [ Ps ]) ⊕ (context P₂ [ Ps ])  ∼⟨ symmetric (SL.≡→∼ (context-[] P₁) SL.⊕-cong SL.≡→∼ (context-[] P₂)) ⟩
      P₁ ⊕ P₂                                    ∼⟨ SL.≡→∼ (context-[] P₁) SL.⊕-cong SL.≡→∼ (context-[] P₂) ⟩■
      (context P₁ [ Qs ]) ⊕ (context P₂ [ Qs ])

    (process P₁) (action {μ = μ₂} {C = C₂} D₂) →
      (context P₁ [ Ps ]) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ symmetric (SL.≡→∼ (context-[] P₁)) SL.⊕-cong (_ ■) ⟩
      P₁ ⊕ μ₂ · (C₂ [ Ps ]′)                   ∼′⟨ ⊕·-cong (D₂ [ Ps≳Qs ]-cong′) ⟩ S.∼:
      P₁ ⊕ μ₂ · (C₂ [ Qs ]′)                   ∼⟨ SL.≡→∼ (context-[] P₁) SL.⊕-cong (_ ■) ⟩■
      (context P₁ [ Qs ]) ⊕ μ₂ · (C₂ [ Qs ]′)

    (action {μ = μ₁} {C = C₁} D₁) (process P₂) →
      μ₁ · (C₁ [ Ps ]′) ⊕ (context P₂ [ Ps ])  ∼⟨ (_ ■) SL.⊕-cong symmetric (SL.≡→∼ (context-[] P₂)) ⟩
      μ₁ · (C₁ [ Ps ]′) ⊕ P₂                   ∼′⟨ ·⊕-cong (D₁ [ Ps≳Qs ]-cong′) ⟩ S.∼:
      μ₁ · (C₁ [ Qs ]′) ⊕ P₂                   ∼⟨ (_ ■) SL.⊕-cong SL.≡→∼ (context-[] P₂) ⟩■
      μ₁ · (C₁ [ Qs ]′) ⊕ (context P₂ [ Qs ])

    (action {μ = μ₁} {C = C₁} D₁) (action {μ = μ₂} {C = C₂} D₂) →
      μ₁ · (C₁ [ Ps ]′) ⊕ μ₂ · (C₂ [ Ps ]′)  ∼⟨ (D₁ [ Ps≳Qs ]-cong′) ·⊕·-cong (D₂ [ Ps≳Qs ]-cong′) ⟩■
      μ₁ · (C₁ [ Qs ]′) ⊕ μ₂ · (C₂ [ Qs ]′)

_[_]-cong′ :
  ∀ {i n Ps Qs} {C : Context ∞ n} →
  Non-degenerate ∞ C → (∀ x → [ i ] Ps x ≳′ Qs x) →
  [ i ] C [ Ps ] ≳′ C [ Qs ]
force (C [ Ps≳Qs ]-cong′) = C [ (λ x → force (Ps≳Qs x)) ]-cong