```------------------------------------------------------------------------
-- Some results/examples related to CCS, implemented using the
-- coinductive definition of bisimilarity
------------------------------------------------------------------------

-- Unless anything else is stated the results (or statements, in the
-- case of exercises) below are taken from "Enhancements of the
-- bisimulation proof method" by Pous and Sangiorgi.

{-# OPTIONS --without-K --safe #-}

module Bisimilarity.CCS.Examples {ℓ} {Name : Set ℓ} where

open import Equality.Propositional
open import Prelude

open import Bisimilarity.CCS
import Bisimilarity.Equational-reasoning-instances
open import Equational-reasoning
open import Labelled-transition-system.CCS Name

open import Bisimilarity CCS

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method"

mutual

-- For a more general result, see 6-2-14 below.

!∙⊕∙∼!∙∣!∙ : ∀ {i a b} → [ i ] ! (a ∙ ⊕ b ∙) ∼ ! a ∙ ∣ ! b ∙
!∙⊕∙∼!∙∣!∙ {i} = ⟨ lr , rl ⟩
where
lemma = λ {a b} → ∼′:
! (a ∙ ⊕ b ∙) ∣ ∅  ∼⟨ ∣-right-identity ⟩ ∼′:
! (a ∙ ⊕ b ∙)      ∼⟨ !∙⊕∙∼′!∙∣!∙ {i = i} ⟩■
! a ∙ ∣ ! b ∙

left-lemma = λ {a b} → ∼′:
! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ lemma ⟩ ∼′:
! a ∙ ∣ ! b ∙        ∼⟨ symmetric ∣-right-identity ∣-cong reflexive ⟩■
(! a ∙ ∣ ∅) ∣ ! b ∙

right-lemma = λ {a b} → ∼′:
! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ lemma ⟩ ∼′:
! a ∙ ∣  ! b ∙       ∼⟨ reflexive ∣-cong symmetric ∣-right-identity ⟩■
! a ∙ ∣ (! b ∙ ∣ ∅)

τ-lemma = λ {a b} → ∼′:
(! (a ∙ ⊕ b ∙) ∣ ∅) ∣ ∅    ∼⟨ ∣-right-identity ⟩
! (a ∙ ⊕ b ∙) ∣ ∅          ∼⟨ lemma ⟩ ∼′:
! a ∙ ∣ ! b ∙              ∼⟨ symmetric (∣-right-identity ∣-cong ∣-right-identity) ⟩■
(! a ∙ ∣ ∅) ∣ (! b ∙ ∣ ∅)

lr : ∀ {a b P μ} →
! (a ∙ ⊕ b ∙) [ μ ]⟶ P →
∃ λ Q → ! a ∙ ∣ ! b ∙ [ μ ]⟶ Q × [ i ] P ∼′ Q
lr {a} {b} {P} tr = case 6-1-3-2 tr of λ where

(inj₁ (.∅ , sum-left action , P∼![a⊕b]∣∅)) →
P                    ∼⟨ P∼![a⊕b]∣∅ ⟩ ∼′:
! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ left-lemma ⟩■
(! a ∙ ∣ ∅) ∣ ! b ∙  [ name a ]⟵⟨ par-left (replication (par-right action)) ⟩
! a ∙       ∣ ! b ∙

(inj₁ (.∅ , sum-right action , P∼![a⊕b]∣∅)) →
P                    ∼⟨ P∼![a⊕b]∣∅ ⟩ ∼′:
! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ right-lemma ⟩■
! a ∙ ∣ (! b ∙ ∣ ∅)  [ name b ]⟵⟨ par-right (replication (par-right action)) ⟩
! a ∙ ∣ ! b ∙

(inj₂ (refl , P′ , P″ , c , a⊕b⟶P′ , a⊕b⟶P″ , P∼![a⊕b]∣P′∣P″)) →
let b≡co-a , P′≡∅ , P″≡∅ = Σ-map id [ id , id ]
(·⊕·-co a⊕b⟶P′ a⊕b⟶P″) in

P                          ∼⟨ P∼![a⊕b]∣P′∣P″ ⟩
(! (a ∙ ⊕ b ∙) ∣ P′) ∣ P″  ∼⟨ (reflexive ∣-cong ≡⇒∼ P′≡∅) ∣-cong ≡⇒∼ P″≡∅ ⟩ ∼′:
(! (a ∙ ⊕ b ∙) ∣ ∅) ∣ ∅    ∼⟨ τ-lemma ⟩■
(! a ∙ ∣ ∅) ∣ (! b ∙ ∣ ∅)  [ τ ]⟵⟨ par-τ′ b≡co-a (replication (par-right action))
(replication (par-right action)) ⟩
! a ∙ ∣ ! b ∙

rl : ∀ {a b Q μ} →
! a ∙ ∣ ! b ∙ [ μ ]⟶ Q →
∃ λ P → ! (a ∙ ⊕ b ∙) [ μ ]⟶ P × [ i ] P ∼′ Q
rl {a} {b} (par-left {P′ = P′} tr) =
case 6-1-3-2 tr of λ where

(inj₁ (.∅ , action , P′∼!a∣∅)) →
! (a ∙ ⊕ b ∙)        [ name a ]⟶⟨ replication (par-right (sum-left action)) ⟩ʳˡ
! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ left-lemma ⟩ ∼′:
(! a ∙ ∣ ∅) ∣ ! b ∙  ∼⟨ symmetric P′∼!a∣∅ ∣-cong reflexive ⟩■
P′ ∣ ! b ∙

(inj₂ (refl , .∅ , P″ , .a , action , a⟶P″ , P′∼!a∣∅∣P″)) →
⊥-elim (names-are-not-inverted a⟶P″)

rl {a} {b} (par-right {Q′ = Q′} tr) =
case 6-1-3-2 tr of λ where

(inj₁ (.∅ , action , Q′∼!b∣∅)) →
! (a ∙ ⊕ b ∙)        [ name b ]⟶⟨ replication (par-right (sum-right action)) ⟩ʳˡ
! (a ∙ ⊕ b ∙) ∣ ∅    ∼⟨ right-lemma ⟩ ∼′:
! a ∙ ∣ (! b ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong symmetric Q′∼!b∣∅ ⟩■
! a ∙ ∣ Q′

(inj₂ (refl , .∅ , Q″ , .b , action , b⟶Q″ , Q′∼!b∣∅∣Q″)) →
⊥-elim (names-are-not-inverted b⟶Q″)

rl {a} (par-τ {P′ = P′} {Q′ = Q′} tr₁ tr₂) =
case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where

(inj₁ (.∅ , action , P′∼!a∣∅) ,
inj₁ (.∅ , action , Q′∼!co-a∣∅)) →
! (a ∙ ⊕ co a ∙)              [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left action)))
(sum-right action)) ⟩ʳˡ
(! (a ∙ ⊕ co a ∙) ∣ ∅) ∣ ∅    ∼⟨ τ-lemma ⟩ ∼′:
(! a ∙ ∣ ∅) ∣ (! co a ∙ ∣ ∅)  ∼⟨ symmetric (P′∼!a∣∅ ∣-cong Q′∼!co-a∣∅) ⟩■
P′ ∣ Q′

(inj₁ _ , inj₂ (() , _))
(inj₂ (() , _) , _)

!∙⊕∙∼′!∙∣!∙ : ∀ {a b i} → [ i ] ! (a ∙ ⊕ b ∙) ∼′ ! a ∙ ∣ ! b ∙
force !∙⊕∙∼′!∙∣!∙ = !∙⊕∙∼!∙∣!∙

------------------------------------------------------------------------
-- Exercise 6.2.4

mutual

-- For a more general result, see 6-2-17-4 below.

6-2-4 : ∀ {a i} → [ i ] ! ! a ∙ ∼ ! a ∙
6-2-4 {a} {i} = ⟨ lr , rl ⟩
where
impossible : ∀ {μ P q} {Q : Set q} →
! ! a ∙ [ μ ]⟶ P → μ ≡ τ → Q
impossible {μ} !!a⟶P μ≡τ = ⊥-elim \$ name≢τ
(name a  ≡⟨ !-only (!-only ·-only) !!a⟶P ⟩
μ       ≡⟨ μ≡τ ⟩∎
τ       ∎)

lemma = λ {P} P∼!a∣∅ → ∼′:
! ! a ∙ ∣ P            ∼⟨ reflexive ∣-cong P∼!a∣∅ ⟩
! ! a ∙ ∣ (! a ∙ ∣ ∅)  ∼⟨ reflexive ∣-cong ∣-right-identity ⟩
! ! a ∙ ∣ ! a ∙        ∼⟨ 6-1-2 ⟩
! ! a ∙                ∼⟨ 6-2-4′ {i = i} ⟩ ∼′:
! a ∙                  ∼⟨ symmetric ∣-right-identity ⟩■
! a ∙ ∣ ∅

lr : ∀ {P μ} →
! ! a ∙ [ μ ]⟶ P →
∃ λ P′ → ! a ∙ [ μ ]⟶ P′ × [ i ] P ∼′ P′
lr {P = P} !!a⟶P = case 6-1-3-2 !!a⟶P of λ where
(inj₂ (μ≡τ , _))               → impossible !!a⟶P μ≡τ
(inj₁ (P′ , !a⟶P′ , P∼!!a∣P′)) → case 6-1-3-2 !a⟶P′ of λ where
(inj₂ (μ≡τ , _))               → impossible !!a⟶P μ≡τ
(inj₁ (.∅ , action , P′∼!a∣∅)) →
P             ∼⟨ P∼!!a∣P′ ⟩ ∼′:
! ! a ∙ ∣ P′  ∼⟨ lemma P′∼!a∣∅ ⟩■
! a ∙ ∣ ∅     [ name a ]⟵⟨ replication (par-right action) ⟩
! a ∙

rl : ∀ {P μ} →
! a ∙ [ μ ]⟶ P →
∃ λ P′ → ! ! a ∙ [ μ ]⟶ P′ × [ i ] P′ ∼′ P
rl {P = P} !a⟶P = case 6-1-3-2 !a⟶P of λ where
(inj₂ (refl , .∅ , Q″ , .a , action , a⟶Q″ , _)) →
⊥-elim (names-are-not-inverted a⟶Q″)
(inj₁ (.∅ , action , P∼!a∣∅)) →
! ! a ∙      [ name a ]⟶⟨ replication (par-right !a⟶P) ⟩ʳˡ
! ! a ∙ ∣ P  ∼⟨ lemma P∼!a∣∅ ⟩ ∼′:
! a ∙ ∣ ∅    ∼⟨ symmetric P∼!a∣∅ ⟩■
P

6-2-4′ : ∀ {a i} → [ i ] ! ! a ∙ ∼′ ! a ∙
force 6-2-4′ = 6-2-4

------------------------------------------------------------------------
-- A result mentioned in "Enhancements of the bisimulation proof
-- method"

∙∣∙∼∙∙ : ∀ {a} → a ∙ ∣ a ∙ ∼ name a ∙ (a ∙)
∙∣∙∼∙∙ {a} = ⟨ lr , rl ⟩
where
lr : ∀ {P μ} → a ∙ ∣ a ∙ [ μ ]⟶ P →
∃ λ P′ → name a ∙ (a ∙) [ μ ]⟶ P′ × P ∼′ P′
lr (par-left action) =
∅ ∣ a ∙         ∼⟨ ∣-left-identity ⟩■
a ∙             [ name a ]⟵⟨ action ⟩
name a ∙ (a ∙)

lr (par-right action) =
a ∙ ∣ ∅         ∼⟨ ∣-right-identity ⟩■
a ∙             [ name a ]⟵⟨ action ⟩
name a ∙ (a ∙)

lr (par-τ action tr) = ⊥-elim (names-are-not-inverted tr)

rl : ∀ {P μ} → name a ∙ (a ∙) [ μ ]⟶ P →
∃ λ P′ → a ∙ ∣ a ∙ [ μ ]⟶ P′ × P′ ∼′ P
rl action =
a ∙ ∣ a ∙  [ name a ]⟶⟨ par-right action ⟩ʳˡ
a ∙ ∣ ∅    ∼⟨ ∣-right-identity ⟩■
a ∙

------------------------------------------------------------------------
-- Lemma 6.2.14

mutual

-- A more general variant of !∙⊕∙∼!∙∣!∙. For an even more general
-- variant, see 6-2-17-2 below.

6-2-14 :
∀ {i a b P Q} →
[ i ] ! (name a ∙ P ⊕ name b ∙ Q) ∼ ! name a ∙ P ∣ ! name b ∙ Q
6-2-14 {i} = ⟨ lr , rl ⟩
where
left-lemma = λ {a b P Q} → ∼′:
! (name a ∙ P ⊕ name b ∙ Q) ∣ P    ∼⟨ 6-2-14′ {i = i} ∣-cong′ reflexive ⟩ ∼′:
(! name a ∙ P ∣ ! name b ∙ Q) ∣ P  ∼⟨ swap-rightmost ⟩■
(! name a ∙ P ∣ P) ∣ ! name b ∙ Q

right-lemma = λ {a b P Q} → ∼′:
! (name a ∙ P ⊕ name b ∙ Q) ∣ Q    ∼⟨ 6-2-14′ {i = i} ∣-cong′ reflexive ⟩ ∼′:
(! name a ∙ P ∣ ! name b ∙ Q) ∣ Q  ∼⟨ symmetric ∣-assoc ⟩■
! name a ∙ P ∣ (! name b ∙ Q ∣ Q)

τ-lemma = λ {a b P Q} → ∼′:
(! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q    ∼⟨ left-lemma ∣-cong′ reflexive ⟩ ∼′:
((! name a ∙ P ∣ P) ∣ ! name b ∙ Q) ∣ Q  ∼⟨ symmetric ∣-assoc ⟩■
(! name a ∙ P ∣ P) ∣ (! name b ∙ Q ∣ Q)

lr : ∀ {a b P Q R μ} →
! (name a ∙ P ⊕ name b ∙ Q) [ μ ]⟶ R →
∃ λ S → ! name a ∙ P ∣ ! name b ∙ Q [ μ ]⟶ S × [ i ] R ∼′ S
lr {a} {b} {P} {Q} {R} tr = case 6-1-3-2 tr of λ where

(inj₁ (.P , sum-left action , R∼![aP⊕bQ]∣P)) →
R                                  ∼⟨ R∼![aP⊕bQ]∣P ⟩ ∼′:
! (name a ∙ P ⊕ name b ∙ Q) ∣ P    ∼⟨ left-lemma ⟩■
(! name a ∙ P ∣ P) ∣ ! name b ∙ Q  [ name a ]⟵⟨ par-left (replication (par-right action)) ⟩
! name a ∙ P       ∣ ! name b ∙ Q

(inj₁ (.Q , sum-right action , R∼![aP⊕bQ]∣Q)) →
R                                  ∼⟨ R∼![aP⊕bQ]∣Q ⟩ ∼′:
! (name a ∙ P ⊕ name b ∙ Q) ∣ Q    ∼⟨ right-lemma ⟩■
! name a ∙ P ∣ (! name b ∙ Q ∣ Q)  [ name b ]⟵⟨ par-right (replication (par-right action)) ⟩
! name a ∙ P ∣ ! name b ∙ Q

(inj₂ ( refl , R′ , R″ , c , aP⊕bQ⟶R′ , aP⊕bQ⟶R″
, R∼![aP⊕bQ]∣R′∣R″
)) →
let b≡co-a , R′≡,R″≡ = ·⊕·-co aP⊕bQ⟶R′ aP⊕bQ⟶R″

lemma : _ → [ _ ] _ ∼ _
lemma = λ where
(inj₁ (R′≡P , R″≡Q)) →
(! (name a ∙ P ⊕ name b ∙ Q) ∣ R′) ∣ R″  ∼⟨ (reflexive ∣-cong ≡⇒∼ R′≡P) ∣-cong ≡⇒∼ R″≡Q ⟩■
(! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q
(inj₂ (R′≡Q , R″≡P)) →
(! (name a ∙ P ⊕ name b ∙ Q) ∣ R′) ∣ R″  ∼⟨ (reflexive ∣-cong ≡⇒∼ R′≡Q) ∣-cong ≡⇒∼ R″≡P ⟩ ∼:
(! (name a ∙ P ⊕ name b ∙ Q) ∣ Q) ∣ P    ∼⟨ swap-rightmost ⟩■
(! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q
in
R                                        ∼⟨ R∼![aP⊕bQ]∣R′∣R″ ⟩
(! (name a ∙ P ⊕ name b ∙ Q) ∣ R′) ∣ R″  ∼⟨ lemma R′≡,R″≡ ⟩ ∼′:
(! (name a ∙ P ⊕ name b ∙ Q) ∣ P) ∣ Q    ∼⟨ τ-lemma ⟩■
(! name a ∙ P ∣ P) ∣ (! name b ∙ Q ∣ Q)  [ τ ]⟵⟨ par-τ′ b≡co-a (replication (par-right action))
(replication (par-right action)) ⟩
! name a ∙ P ∣ ! name b ∙ Q

rl : ∀ {a b P Q S μ} →
! name a ∙ P ∣ ! name b ∙ Q [ μ ]⟶ S →
∃ λ R → ! (name a ∙ P ⊕ name b ∙ Q) [ μ ]⟶ R × [ i ] R ∼′ S
rl {a} {b} {P} {Q} (par-left {P′ = S} tr) =
case 6-1-3-2 tr of λ where
(inj₁ (.P , action , S∼!aP∣P)) →
! (name a ∙ P ⊕ name b ∙ Q)        [ name a ]⟶⟨ replication (par-right (sum-left action)) ⟩ʳˡ
! (name a ∙ P ⊕ name b ∙ Q) ∣ P    ∼⟨ left-lemma ⟩ ∼′:
(! name a ∙ P ∣ P) ∣ ! name b ∙ Q  ∼⟨ symmetric S∼!aP∣P ∣-cong reflexive ⟩■
S ∣ ! name b ∙ Q

(inj₂ (refl , .P , S′ , .a , action , aP⟶S′ , S∼!aP∣P∣S′)) →
⊥-elim (names-are-not-inverted aP⟶S′)

rl {a} {b} {P} {Q} (par-right {Q′ = S} tr) =
case 6-1-3-2 tr of λ where
(inj₁ (.Q , action , S∼!bQ∣Q)) →
! (name a ∙ P ⊕ name b ∙ Q)        [ name b ]⟶⟨ replication (par-right (sum-right action)) ⟩ʳˡ
! (name a ∙ P ⊕ name b ∙ Q) ∣ Q    ∼⟨ right-lemma ⟩ ∼′:
! name a ∙ P ∣ (! name b ∙ Q ∣ Q)  ∼⟨ reflexive ∣-cong symmetric S∼!bQ∣Q ⟩■
! name a ∙ P ∣ S

(inj₂ (refl , .Q , S′ , .b , action , bQ⟶S′ , S∼!bQ∣Q∣S′)) →
⊥-elim (names-are-not-inverted bQ⟶S′)

rl {a} {P = P} {Q} (par-τ {P′ = S} {Q′ = S′} tr₁ tr₂) =
case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
(inj₁ (.P , action , S∼!aP∣P) ,
inj₁ (.Q , action , S′∼!co-aQ∣Q)) →
! (name a ∙ P ⊕ name (co a) ∙ Q)              [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left action)))
(sum-right action)) ⟩ʳˡ
(! (name a ∙ P ⊕ name (co a) ∙ Q) ∣ P) ∣ Q    ∼⟨ τ-lemma ⟩ ∼′:
(! name a ∙ P ∣ P) ∣ (! name (co a) ∙ Q ∣ Q)  ∼⟨ symmetric (S∼!aP∣P ∣-cong S′∼!co-aQ∣Q) ⟩■
S ∣ S′

(inj₁ _ , inj₂ (() , _))
(inj₂ (() , _) , _)

6-2-14′ :
∀ {i a b P Q} →
[ i ] ! (name a ∙ P ⊕ name b ∙ Q) ∼′ ! name a ∙ P ∣ ! name b ∙ Q
force 6-2-14′ = 6-2-14

------------------------------------------------------------------------
-- Lemma 6.2.17

-- Some results mentioned in the proof of 6.2.17 (1) in
-- "Enhancements of the bisimulation proof method".

6-2-17-1-lemma₁ : ∀ {P Q} → (! P ∣ ! Q) ∣ (P ∣ Q) ∼ ! P ∣ ! Q
6-2-17-1-lemma₁ {P} {Q} =
(! P ∣ ! Q) ∣ (P ∣ Q)  ∼⟨ swap-in-the-middle ⟩ ∼:
(! P ∣ P) ∣ (! Q ∣ Q)  ∼⟨ 6-1-2 ∣-cong 6-1-2 ⟩■
! P ∣ ! Q

abstract

6-2-17-1-lemma₂ :
∀ {P Q R μ} →
! (P ∣ Q) [ μ ]⟶ R →
∃ λ S →
R ∼ ! (P ∣ Q) ∣ S ×
∃ λ T →
! P ∣ ! Q [ μ ]⟶ T ×
(! P ∣ ! Q) ∣ S ∼′ T
6-2-17-1-lemma₂ {P} {Q} {R} tr = case 6-1-3-2 tr of λ where
(inj₁ (R′ , P∣Q⟶R′ , R∼![P∣Q]∣R′)) →
let R″ , !P∣!Q⟶R″ , !P∣!Q∣R′∼R″ =
left-to-right
((! P ∣ ! Q) ∣ (P ∣ Q)  ∼⟨ 6-2-17-1-lemma₁ ⟩■
! P ∣ ! Q)
((! P ∣ ! Q) ∣ (P ∣ Q)  ⟶⟨ par-right P∣Q⟶R′ ⟩
(! P ∣ ! Q) ∣ R′)
in _ , R∼![P∣Q]∣R′ , _ , !P∣!Q⟶R″ , !P∣!Q∣R′∼R″

(inj₂ (refl , R′ , R″ , a , P∣Q⟶R′ , P∣Q⟶R″ , R∼![P∣Q]∣R′∣R″)) →
let T , !P∣!Q⟶T , !P∣!Q∣[R′∣R″]∼T =
left-to-right
((! P ∣ ! Q) ∣ ((P ∣ Q) ∣ (P ∣ Q))  ∼⟨ ∣-assoc ⟩
((! P ∣ ! Q) ∣ (P ∣ Q)) ∣ (P ∣ Q)  ∼⟨ 6-2-17-1-lemma₁ ∣-cong reflexive ⟩ ∼:
(! P ∣ ! Q) ∣ (P ∣ Q)              ∼⟨ 6-2-17-1-lemma₁ ⟩■
! P ∣ ! Q)
((! P ∣ ! Q) ∣ ((P ∣ Q) ∣ (P ∣ Q))  ⟶⟨ par-right (par-τ P∣Q⟶R′ P∣Q⟶R″) ⟩
(! P ∣ ! Q) ∣ (R′ ∣ R″))
in
_
, (R                      ∼⟨ R∼![P∣Q]∣R′∣R″ ⟩ ∼:
(! (P ∣ Q) ∣ R′) ∣ R″  ∼⟨ symmetric ∣-assoc ⟩■
! (P ∣ Q) ∣ (R′ ∣ R″))
, _
, !P∣!Q⟶T
, !P∣!Q∣[R′∣R″]∼T

mutual

6-2-17-1 : ∀ {i P Q} → [ i ] ! (P ∣ Q) ∼ ! P ∣ ! Q
6-2-17-1 {i} = ⟨ lr , rl ⟩
where
lr : ∀ {P Q R μ} →
! (P ∣ Q) [ μ ]⟶ R →
∃ λ S → ! P ∣ ! Q [ μ ]⟶ S × [ i ] R ∼′ S
lr {P} {Q} {R} tr =
let S , R∼![P∣Q]∣S , T , !P∣!Q⟶T , !P∣!Q∣S∼T =
6-2-17-1-lemma₂ tr in

R                ∼⟨ R∼![P∣Q]∣S ⟩
! (P ∣ Q) ∣ S    ∼⟨ 6-2-17-1′ ∣-cong′ reflexive ⟩ ∼′:
(! P ∣ ! Q) ∣ S  ∼⟨ !P∣!Q∣S∼T ⟩■
T                ⟵⟨ !P∣!Q⟶T ⟩
! P ∣ ! Q

lemma = λ {P Q R S} → ∼′:
! (P ∣ Q) ∣ (R ∣ S)    ∼⟨ 6-2-17-1′ {i = i} ∣-cong′ reflexive ⟩ ∼′:
(! P ∣ ! Q) ∣ (R ∣ S)  ∼⟨ swap-in-the-middle ⟩■
(! P ∣ R) ∣ (! Q ∣ S)

left-lemma = λ {P Q R} → ∼′:
! (P ∣ Q) ∣ (R ∣ Q)    ∼⟨ lemma ⟩ ∼′:
(! P ∣ R) ∣ (! Q ∣ Q)  ∼⟨ reflexive ∣-cong 6-1-2 ⟩■
(! P ∣ R) ∣ ! Q

right-lemma = λ {P Q R} → ∼′:
! (P ∣ Q) ∣ (P ∣ R)    ∼⟨ lemma ⟩ ∼′:
(! P ∣ P) ∣ (! Q ∣ R)  ∼⟨ 6-1-2 ∣-cong reflexive ⟩■
! P ∣ (! Q ∣ R)

rl : ∀ {P Q S μ} →
! P ∣ ! Q [ μ ]⟶ S →
∃ λ R → ! (P ∣ Q) [ μ ]⟶ R × [ i ] R ∼′ S
rl {P} {Q} (par-left {P′ = S} !P⟶S) =
case 6-1-3-2 !P⟶S
return (const \$ ∃ λ _ → _ × [ i ] _ ∼′ _)
of λ where
(inj₁ (P′ , P⟶P′ , S∼!P∣P′)) →
! (P ∣ Q)             ⟶⟨ replication (par-right (par-left P⟶P′)) ⟩ʳˡ
! (P ∣ Q) ∣ (P′ ∣ Q)  ∼⟨ left-lemma ⟩ ∼′:
(! P ∣ P′) ∣ ! Q      ∼⟨ symmetric S∼!P∣P′ ∣-cong reflexive ⟩■
S ∣ ! Q

(inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , S∼!P∣P′∣P″)) →
! (P ∣ Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-left P⟶P′)))
(par-left P⟶P″)) ⟩ʳˡ
(! (P ∣ Q) ∣ (P′ ∣ Q)) ∣ (P″ ∣ Q)  ∼⟨ left-lemma ∣-cong′ reflexive ⟩
((! P ∣ P′) ∣ ! Q) ∣ (P″ ∣ Q)      ∼⟨ swap-in-the-middle ⟩
((! P ∣ P′) ∣ P″) ∣ (! Q ∣ Q)      ∼⟨ reflexive ∣-cong 6-1-2 ⟩ ∼′:
((! P ∣ P′) ∣ P″) ∣ ! Q            ∼⟨ symmetric S∼!P∣P′∣P″ ∣-cong reflexive ⟩■
S ∣ ! Q

rl {P} {Q} (par-right {Q′ = S} !Q⟶S) =
case 6-1-3-2 !Q⟶S
return (const \$ ∃ λ _ → _ × [ i ] _ ∼′ _)
of λ where
(inj₁ (Q′ , Q⟶Q′ , S∼!Q∣Q′)) →
! (P ∣ Q)             ⟶⟨ replication (par-right (par-right Q⟶Q′)) ⟩ʳˡ
! (P ∣ Q) ∣ (P ∣ Q′)  ∼⟨ right-lemma ⟩ ∼′:
! P ∣ (! Q ∣ Q′)      ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′ ⟩■
! P ∣ S

(inj₂ (refl , Q′ , Q″ , a , Q⟶Q′ , Q⟶Q″ , S∼!Q∣Q′∣Q″)) →
! (P ∣ Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-right Q⟶Q′)))
(par-right Q⟶Q″)) ⟩ʳˡ
(! (P ∣ Q) ∣ (P ∣ Q′)) ∣ (P ∣ Q″)  ∼⟨ right-lemma ∣-cong′ reflexive ⟩
(! P ∣ (! Q ∣ Q′)) ∣ (P ∣ Q″)      ∼⟨ swap-in-the-middle ⟩
(! P ∣ P) ∣ ((! Q ∣ Q′) ∣ Q″)      ∼⟨ 6-1-2 ∣-cong reflexive ⟩ ∼′:
! P ∣ ((! Q ∣ Q′) ∣ Q″)            ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′∣Q″ ⟩■
! P ∣ S

rl {P} {Q} (par-τ {P′ = S} {Q′ = S′} !P⟶S !Q⟶S′) =
case 6-1-3-2 !P⟶S ,′ 6-1-3-2 !Q⟶S′ of λ where
(inj₁ (P′ , P⟶P′ , S∼!P∣P′) ,
inj₁ (Q′ , Q⟶Q′ , S′∼!Q∣Q′)) →
! (P ∣ Q)                          [ τ ]⟶⟨ replication (par-τ (replication (par-right (par-left P⟶P′)))
(par-right Q⟶Q′)) ⟩ʳˡ
(! (P ∣ Q) ∣ (P′ ∣ Q)) ∣ (P ∣ Q′)  ∼⟨ left-lemma ∣-cong′ reflexive ⟩
((! P ∣ P′) ∣ ! Q) ∣ (P ∣ Q′)      ∼⟨ swap-in-the-middle ⟩
((! P ∣ P′) ∣ P) ∣ (! Q ∣ Q′)      ∼⟨ swap-rightmost ∣-cong reflexive ⟩
((! P ∣ P) ∣ P′) ∣ (! Q ∣ Q′)      ∼⟨ (6-1-2 ∣-cong reflexive) ∣-cong reflexive ⟩ ∼′:
(! P ∣ P′) ∣ (! Q ∣ Q′)            ∼⟨ symmetric (S∼!P∣P′ ∣-cong S′∼!Q∣Q′) ⟩■
S ∣ S′

(inj₁ _ , inj₂ (() , _))
(inj₂ (() , _) , _)

6-2-17-1′ : ∀ {i P Q} → [ i ] ! (P ∣ Q) ∼′ ! P ∣ ! Q
force 6-2-17-1′ = 6-2-17-1

mutual

6-2-17-2 : ∀ {i P Q} → [ i ] ! (P ⊕ Q) ∼ ! P ∣ ! Q
6-2-17-2 {i} = ⟨ lr , rl ⟩
where
left-lemma = λ {P Q R} → ∼′:
! (P ⊕ Q) ∣ R    ∼⟨ 6-2-17-2′ {i = i} ∣-cong′ reflexive ⟩ ∼′:
(! P ∣ ! Q) ∣ R  ∼⟨ swap-rightmost ⟩■
(! P ∣ R) ∣ ! Q

right-lemma = λ {P Q R} → ∼′:
! (P ⊕ Q) ∣ R    ∼⟨ 6-2-17-2′ {i = i} ∣-cong′ reflexive ⟩ ∼′:
(! P ∣ ! Q) ∣ R  ∼⟨ symmetric ∣-assoc ⟩■
! P ∣ (! Q ∣ R)

τ-lemma₁ = λ {P P′ P″ Q} → ∼′:
(! (P ⊕ Q) ∣ P′) ∣ P″    ∼⟨ left-lemma ∣-cong′ reflexive ⟩ ∼′:
((! P ∣ P′) ∣ ! Q) ∣ P″  ∼⟨ swap-rightmost ⟩■
((! P ∣ P′) ∣ P″) ∣ ! Q

τ-lemma₂ = λ {P P′ Q Q′} → ∼′:
(! (P ⊕ Q) ∣ P′) ∣ Q′    ∼⟨ left-lemma ∣-cong′ reflexive ⟩ ∼′:
((! P ∣ P′) ∣ ! Q) ∣ Q′  ∼⟨ symmetric ∣-assoc ⟩■
(! P ∣ P′) ∣ (! Q ∣ Q′)

τ-lemma₃ = λ {P Q Q′ Q″} → ∼′:
(! (P ⊕ Q) ∣ Q′) ∣ Q″    ∼⟨ right-lemma ∣-cong′ reflexive ⟩ ∼′:
(! P ∣ (! Q ∣ Q′)) ∣ Q″  ∼⟨ symmetric ∣-assoc ⟩■
! P ∣ ((! Q ∣ Q′) ∣ Q″)

lr : ∀ {P Q R μ} →
! (P ⊕ Q) [ μ ]⟶ R →
∃ λ S → ! P ∣ ! Q [ μ ]⟶ S × [ i ] R ∼′ S
lr {P} {Q} {R} tr =
case 6-1-3-2 tr
return (const \$ ∃ λ _ → _ × [ i ] _ ∼′ _)
of λ where

(inj₁ (P′ , sum-left P⟶P′ , R∼![P⊕Q]∣P′)) →
R                 ∼⟨ R∼![P⊕Q]∣P′ ⟩ ∼′:
! (P ⊕ Q) ∣ P′    ∼⟨ left-lemma ⟩■
(! P ∣ P′) ∣ ! Q  ⟵⟨ par-left (replication (par-right P⟶P′)) ⟩
! P        ∣ ! Q

(inj₁ (Q′ , sum-right Q⟶Q′ , R∼![P⊕Q]∣Q′)) →
R                 ∼⟨ R∼![P⊕Q]∣Q′ ⟩ ∼′:
! (P ⊕ Q) ∣ Q′    ∼⟨ right-lemma ⟩■
! P ∣ (! Q ∣ Q′)  ⟵⟨ par-right (replication (par-right Q⟶Q′)) ⟩
! P ∣  ! Q

(inj₂ ( refl , P′ , P″ , c
, sum-left P⟶P′ , sum-left P⟶P″
, R∼![P⊕Q]∣P′∣P″
)) →
R                        ∼⟨ R∼![P⊕Q]∣P′∣P″ ⟩ ∼′:
(! (P ⊕ Q) ∣ P′) ∣ P″    ∼⟨ τ-lemma₁ ⟩■
((! P ∣ P′) ∣ P″) ∣ ! Q  [ τ ]⟵⟨ par-left (replication (par-τ (replication (par-right P⟶P′)) P⟶P″)) ⟩
! P ∣ ! Q

(inj₂ ( refl , P′ , Q′ , c
, sum-left P⟶P′ , sum-right Q⟶Q′
, R∼![P⊕Q]∣P′∣Q′
)) →
R                        ∼⟨ R∼![P⊕Q]∣P′∣Q′ ⟩ ∼′:
(! (P ⊕ Q) ∣ P′) ∣ Q′    ∼⟨ τ-lemma₂ ⟩■
(! P ∣ P′) ∣ (! Q ∣ Q′)  [ τ ]⟵⟨ par-τ (replication (par-right P⟶P′))
(replication (par-right Q⟶Q′)) ⟩
! P ∣ ! Q

(inj₂ ( refl , Q′ , P′ , c
, sum-right Q⟶Q′ , sum-left P⟶P′
, R∼![P⊕Q]∣Q′∣P′
)) →
R                        ∼⟨ R∼![P⊕Q]∣Q′∣P′ ⟩
(! (P ⊕ Q) ∣ Q′) ∣ P′    ∼⟨ right-lemma ∣-cong′ reflexive ⟩ ∼′:
(! P ∣ (! Q ∣ Q′)) ∣ P′  ∼⟨ swap-rightmost ⟩■
(! P ∣ P′) ∣ (! Q ∣ Q′)  [ τ ]⟵⟨ par-τ′ (sym \$ co-involutive c)
(replication (par-right P⟶P′))
(replication (par-right Q⟶Q′)) ⟩
! P ∣ ! Q

(inj₂ ( refl , Q′ , Q″ , c
, sum-right Q⟶Q′ , sum-right Q⟶Q″
, R∼![P⊕Q]∣Q′∣Q″
)) →
R                        ∼⟨ R∼![P⊕Q]∣Q′∣Q″ ⟩ ∼′:
(! (P ⊕ Q) ∣ Q′) ∣ Q″    ∼⟨ τ-lemma₃ ⟩■
! P ∣ ((! Q ∣ Q′) ∣ Q″)  [ τ ]⟵⟨ par-right (replication (par-τ (replication (par-right Q⟶Q′)) Q⟶Q″)) ⟩
! P ∣ ! Q

rl : ∀ {P Q S μ} →
! P ∣ ! Q [ μ ]⟶ S →
∃ λ R → ! (P ⊕ Q) [ μ ]⟶ R × [ i ] R ∼′ S
rl {P} {Q} (par-left {P′ = S} !P⟶S) =
case 6-1-3-2 !P⟶S
return (const \$ ∃ λ _ → _ × [ i ] _ ∼′ _)
of λ where
(inj₁ (P′ , P⟶P′ , S∼!P∣P′)) →
! (P ⊕ Q)         ⟶⟨ replication (par-right (sum-left P⟶P′)) ⟩ʳˡ
! (P ⊕ Q) ∣ P′    ∼⟨ left-lemma ⟩ ∼′:
(! P ∣ P′) ∣ ! Q  ∼⟨ symmetric S∼!P∣P′ ∣-cong reflexive ⟩■
S ∣ ! Q

(inj₂ (refl , P′ , P″ , a , P⟶P′ , P⟶P″ , S∼!P∣P′∣P″)) →
! (P ⊕ Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left P⟶P′)))
(sum-left P⟶P″)) ⟩ʳˡ
(! (P ⊕ Q) ∣ P′) ∣ P″    ∼⟨ τ-lemma₁ ⟩ ∼′:
((! P ∣ P′) ∣ P″) ∣ ! Q  ∼⟨ symmetric S∼!P∣P′∣P″ ∣-cong reflexive ⟩■
S ∣ ! Q

rl {P} {Q} (par-right {Q′ = S} !Q⟶S) =
case 6-1-3-2 !Q⟶S
return (const \$ ∃ λ _ → _ × [ i ] _ ∼′ _)
of λ where
(inj₁ (Q′ , Q⟶Q′ , S∼!Q∣Q′)) →
! (P ⊕ Q)         ⟶⟨ replication (par-right (sum-right Q⟶Q′)) ⟩ʳˡ
! (P ⊕ Q) ∣ Q′    ∼⟨ right-lemma ⟩ ∼′:
! P ∣ (! Q ∣ Q′)  ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′ ⟩■
! P ∣ S

(inj₂ (refl , Q′ , Q″ , a , Q⟶Q′ , Q⟶Q″ , S∼!Q∣Q′∣Q″)) →
! (P ⊕ Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-right Q⟶Q′)))
(sum-right Q⟶Q″)) ⟩ʳˡ
(! (P ⊕ Q) ∣ Q′) ∣ Q″    ∼⟨ τ-lemma₃ ⟩ ∼′:
! P ∣ ((! Q ∣ Q′) ∣ Q″)  ∼⟨ reflexive ∣-cong symmetric S∼!Q∣Q′∣Q″ ⟩■
! P ∣ S

rl {P} {Q} (par-τ {P′ = S} {Q′ = S′} !P⟶S !Q⟶S′) =
case 6-1-3-2 !P⟶S ,′ 6-1-3-2 !Q⟶S′ of λ where
(inj₁ (P′ , P⟶P′ , S∼!P∣P′) ,
inj₁ (Q′ , Q⟶Q′ , S′∼!Q∣Q′)) →
! (P ⊕ Q)                [ τ ]⟶⟨ replication (par-τ (replication (par-right (sum-left P⟶P′)))
(sum-right Q⟶Q′)) ⟩ʳˡ
(! (P ⊕ Q) ∣ P′) ∣ Q′    ∼⟨ τ-lemma₂ ⟩ ∼′:
(! P ∣ P′) ∣ (! Q ∣ Q′)  ∼⟨ symmetric (S∼!P∣P′ ∣-cong S′∼!Q∣Q′) ⟩■
S ∣ S′

(inj₁ _ , inj₂ (() , _))
(inj₂ (() , _) , _)

6-2-17-2′ : ∀ {i P Q} → [ i ] ! (P ⊕ Q) ∼′ ! P ∣ ! Q
force 6-2-17-2′ = 6-2-17-2

6-2-17-3 : ∀ {P} → ! P ∣ ! P ∼ ! P
6-2-17-3 {P} =
! P ∣ ! P  ∼⟨ symmetric 6-2-17-2 ⟩ ∼:
! (P ⊕ P)  ∼⟨ !-cong ⊕-idempotent ⟩■
! P

-- A result mentioned in the proof of 6.2.17 (4) in "Enhancements of
-- the bisimulation proof method".

6-2-17-4-lemma : ∀ {P Q μ} → ! P [ μ ]⟶ Q → Q ∼ ! P ∣ Q
6-2-17-4-lemma {P} {Q} !P⟶Q = case 6-1-3-2 !P⟶Q of λ where
(inj₁ (P′ , P⟶P′ , Q∼!P∣P′)) →
Q                 ∼⟨ Q∼!P∣P′ ⟩
! P ∣ P′          ∼⟨ symmetric 6-2-17-3 ∣-cong reflexive ⟩
(! P ∣ ! P) ∣ P′  ∼⟨ symmetric ∣-assoc ⟩ ∼:
! P ∣ (! P ∣ P′)  ∼⟨ reflexive ∣-cong symmetric Q∼!P∣P′ ⟩■
! P ∣ Q

(inj₂ (_ , P′ , P″ , _ , P⟶P′ , P⟶P″ , Q∼!P∣P′∣P″)) →
Q                        ∼⟨ Q∼!P∣P′∣P″ ⟩
(! P ∣ P′) ∣ P″          ∼⟨ symmetric ∣-assoc ⟩
! P ∣ (P′ ∣ P″)          ∼⟨ symmetric 6-2-17-3 ∣-cong reflexive ⟩
(! P ∣ ! P) ∣ (P′ ∣ P″)  ∼⟨ symmetric ∣-assoc ⟩
! P ∣ (! P ∣ (P′ ∣ P″))  ∼⟨ reflexive ∣-cong ∣-assoc ⟩ ∼:
! P ∣ ((! P ∣ P′) ∣ P″)  ∼⟨ reflexive ∣-cong symmetric Q∼!P∣P′∣P″ ⟩■
! P ∣ Q

mutual

6-2-17-4 : ∀ {P i} → [ i ] ! ! P ∼ ! P
6-2-17-4 {P} {i} = ⟨ lr , rl ⟩
where
lemma = λ {Q μ} (!P⟶Q : ! P [ μ ]⟶ Q) → ∼′:
! ! P ∣ Q  ∼⟨ 6-2-17-4′ {i = i} ∣-cong′ reflexive ⟩ ∼′:
! P ∣ Q    ∼⟨ symmetric (6-2-17-4-lemma !P⟶Q) ⟩■
Q

lr : ∀ {Q μ} →
! ! P [ μ ]⟶ Q →
∃ λ Q′ → ! P [ μ ]⟶ Q′ × [ i ] Q ∼′ Q′
lr {Q} !!P⟶Q = case 6-1-3-2 !!P⟶Q of λ where
(inj₁ (Q′ , !P⟶Q′ , Q∼!!P∣Q′)) →
Q           ∼⟨ Q∼!!P∣Q′ ⟩ ∼′:
! ! P ∣ Q′  ∼⟨ lemma !P⟶Q′ ⟩■
Q′          ⟵⟨ !P⟶Q′ ⟩
! P

(inj₂ (refl , Q′ , Q″ , a , !P⟶Q′ , !P⟶Q″ , Q∼!!P∣Q′∣Q″)) →
case 6-1-3-2 !P⟶Q″ of λ where
(inj₂ (() , _))
(inj₁ (Q‴ , P⟶Q‴ , Q″∼!P∣Q‴)) →
let !P⟶Q′∣Q″ =
! P      [ τ ]⟶⟨ replication (par-τ !P⟶Q′ P⟶Q‴) ⟩
Q′ ∣ Q‴
in
Q                          ∼⟨ Q∼!!P∣Q′∣Q″ ⟩
(! ! P ∣ Q′) ∣ Q″          ∼⟨ reflexive ∣-cong Q″∼!P∣Q‴ ⟩
(! ! P ∣ Q′) ∣ (! P ∣ Q‴)  ∼⟨ swap-in-the-middle ⟩
(! ! P ∣ ! P) ∣ (Q′ ∣ Q‴)  ∼⟨ 6-1-2 ∣-cong reflexive ⟩ ∼′:
! ! P ∣ (Q′ ∣ Q‴)          ∼⟨ lemma !P⟶Q′∣Q″ ⟩■
Q′ ∣ Q‴                    [ τ ]⟵⟨ !P⟶Q′∣Q″ ⟩
! P

rl : ∀ {Q μ} →
! P [ μ ]⟶ Q →
∃ λ Q′ → ! ! P [ μ ]⟶ Q′ × [ i ] Q′ ∼′ Q
rl {Q} !P⟶Q =
! ! P      ⟶⟨ replication (par-right !P⟶Q) ⟩ʳˡ
! ! P ∣ Q  ∼⟨ lemma !P⟶Q ⟩■
Q

6-2-17-4′ : ∀ {P i} → [ i ] ! ! P ∼′ ! P
force 6-2-17-4′ = 6-2-17-4

------------------------------------------------------------------------
-- An example from "Coinduction All the Way Up" by Pous

module _ (a b : Name-with-kind) where

A B C D : ∀ {i} → Proc i

A = name a ∙ name b ∙ D
B = name a ∙ name b ∙ C

C = name (co a) · λ { .force → A ∣ C }
D = name (co a) · λ { .force → B ∣ D }

mutual

A∼B : ∀ {i} → [ i ] A ∼ B
A∼B = refl ∙-cong (refl ∙-cong symmetric C∼D)

C∼D : ∀ {i} → [ i ] C ∼ D
C∼D = refl ·-cong λ { .force → A∼B ∣-cong C∼D }

------------------------------------------------------------------------
-- Another example (not taken from Pous and Sangiorgi)

Restricted : Name → Proc ∞
Restricted a = ⟨ν a ⟩ (name (a , true) · λ { .force → ∅ })

Restricted∼∅ : ∀ {a} → Restricted a ∼ ∅
Restricted∼∅ =
⟨ (λ { (restriction x≢x action) → ⊥-elim (x≢x refl) })
, (λ ())
⟩
```