{-# OPTIONS --sized-types #-}
open import Prelude hiding (module W; step-→)
module Bisimilarity.Weak.CCS.Examples {ℓ} {Name : Type ℓ} where
open import Equality.Propositional
open import Function-universe equality-with-J hiding (id; _∘_)
open import Bisimilarity.CCS
import Bisimilarity.Equational-reasoning-instances
import Bisimilarity.Weak.CCS as WL
import Bisimilarity.Weak.Equational-reasoning-instances
open import Equational-reasoning
import Expansion.CCS as EL
import Expansion.Equational-reasoning-instances
open import Labelled-transition-system.CCS Name
open import Bisimilarity CCS using (_∼_; ∼:_)
open import Bisimilarity.Weak CCS as W
open import Expansion CCS as E
import Labelled-transition-system.Equational-reasoning-instances CCS
as Dummy
mutual
6-5-4 :
∀ {i a b} →
[ i ] ! name a ∙ (b ∙) ∣ ! co a ∙ ≈ (! a ∙ ∣ ! b ∙) ∣ ! co a ∙
6-5-4 {i} {a} {b} = W.⟨ lr , rl ⟩
where
lemma =
(! a ∙ ∣ ! b ∙) ∣ b ∙ ∼⟨ symmetric ∣-assoc ⟩
! a ∙ ∣ (! b ∙ ∣ b ∙) ∼⟨ symmetric ∣-right-identity ∣-cong 6-1-2 ⟩■
(! a ∙ ∣ ∅) ∣ ! b ∙
lr :
∀ {P μ} →
! name a ∙ (b ∙) ∣ ! co a ∙ [ μ ]⟶ P →
∃ λ Q → (! a ∙ ∣ ! b ∙) ∣ ! co a ∙ [ μ ]⇒̂ Q × [ i ] P ≈′ Q
lr (par-left {P′ = P} tr) = case 6-1-3-2 tr of λ where
(inj₁ (.(b ∙) , action , P∼!ab∣b)) →
P ∣ ! co a ∙ ∼⟨ P∼!ab∣b ∣-cong reflexive ⟩
(! name a ∙ (b ∙) ∣ b ∙) ∣ ! co a ∙ ∼⟨ swap-rightmost ⟩
(! name a ∙ (b ∙) ∣ ! co a ∙) ∣ b ∙ ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ b ∙ ∼⟨ swap-rightmost ⟩ ∼:
((! a ∙ ∣ ! b ∙) ∣ b ∙) ∣ ! co a ∙ ∼⟨ lemma ∣-cong reflexive ⟩■
((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ ! co a ∙
W.⇐̂[ name a ] ←⟨ ⟶: par-left (par-left (replication (par-right action))) ⟩■
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙
(inj₂ (_ , .(b ∙) , _ , .a , action , ab[a̅]⟶ , _)) →
⊥-elim (names-are-not-inverted ab[a̅]⟶)
lr (par-right {Q′ = Q} tr) = case 6-1-3-2 tr of λ where
(inj₁ (.∅ , action , Q∼!a̅∣∅)) →
! name a ∙ (b ∙) ∣ Q ∼⟨ reflexive ∣-cong Q∼!a̅∣∅ ⟩
! name a ∙ (b ∙) ∣ (! co a ∙ ∣ ∅) ∼⟨ ∣-assoc ⟩
(! name a ∙ (b ∙) ∣ ! co a ∙) ∣ ∅ ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩ ∼:
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ ∅ ∼⟨ symmetric ∣-assoc ⟩■
(! a ∙ ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅)
W.⇐̂[ name (co a) ] ←⟨ ⟶: par-right (replication (par-right action)) ⟩■
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙
(inj₂ (_ , .∅ , _ , .(co a) , action , a̅[a̅̅]⟶ , _)) →
⊥-elim (names-are-not-inverted a̅[a̅̅]⟶)
lr (par-τ {P′ = P} {Q′ = Q} tr₁ tr₂) =
case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
(inj₁ (.(b ∙) , action , P∼!ab∣b) ,
inj₁ (R , tr , Q∼!a̅∣R)) →
P ∣ Q ∼⟨ P∼!ab∣b ∣-cong Q∼!a̅∣R ⟩
(! name a ∙ (b ∙) ∣ b ∙) ∣ (! co a ∙ ∣ R) ∼≡⟨ cong (λ R → _ ∣ (_ ∣ R)) (·-only⟶ tr) ⟩
(! name a ∙ (b ∙) ∣ b ∙) ∣ (! co a ∙ ∣ ∅) ∼⟨ swap-in-the-middle ⟩
(! name a ∙ (b ∙) ∣ ! co a ∙) ∣ (b ∙ ∣ ∅) ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ (b ∙ ∣ ∅) ∼⟨ swap-in-the-middle ⟩ ∼:
((! a ∙ ∣ ! b ∙) ∣ b ∙) ∣ (! co a ∙ ∣ ∅) ∼⟨ lemma ∣-cong reflexive ⟩■
((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅)
W.⇐̂[ τ ] ←⟨ par-τ (par-left (replication (par-right action)))
(replication (par-right action)) ⟩■
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙
(_ , inj₂ (() , _))
(inj₂ (() , _) , _)
rl-lemma :
∀ {Q μ} →
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ [ μ ]⟶ Q →
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼ Q
×
(μ ≡ name a ⊎ μ ≡ name b ⊎ μ ≡ name (co a) ⊎ μ ≡ τ)
rl-lemma (par-left (par-left {P′ = P} tr)) =
case 6-1-3-2 tr of λ where
(inj₁ (.∅ , action , P∼!a∣∅)) →
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ (symmetric ∣-right-identity ∣-cong reflexive) ∣-cong reflexive ⟩
((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ (symmetric P∼!a∣∅ ∣-cong reflexive) ∣-cong reflexive ⟩■
(P ∣ ! b ∙) ∣ ! co a ∙)
, inj₁ refl
(inj₂ (refl , .∅ , _ , .a , action , a[a̅]⟶ , _)) →
⊥-elim (names-are-not-inverted a[a̅]⟶)
rl-lemma (par-left (par-right {Q′ = P} tr)) =
case 6-1-3-2 tr of λ where
(inj₁ (.∅ , action , P∼!b∣∅)) →
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ (reflexive ∣-cong symmetric ∣-right-identity) ∣-cong reflexive ⟩
(! a ∙ ∣ (! b ∙ ∣ ∅)) ∣ ! co a ∙ ∼⟨ (reflexive ∣-cong symmetric P∼!b∣∅) ∣-cong reflexive ⟩■
(! a ∙ ∣ P) ∣ ! co a ∙)
, inj₂ (inj₁ refl)
(inj₂ (_ , .∅ , _ , .b , action , b[b̅]⟶ , _)) →
⊥-elim (names-are-not-inverted b[b̅]⟶)
rl-lemma (par-left (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∼!b∣∅)) →
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ symmetric (∣-right-identity ∣-cong ∣-right-identity) ∣-cong reflexive ⟩
((! a ∙ ∣ ∅) ∣ (! b ∙ ∣ ∅)) ∣ ! co a ∙ ∼⟨ symmetric (P∼!a∣∅ ∣-cong Q∼!b∣∅) ∣-cong reflexive ⟩■
(P ∣ Q) ∣ ! co a ∙)
, inj₂ (inj₂ (inj₂ refl))
(inj₂ (() , _) , _)
(_ , inj₂ (() , _))
rl-lemma (par-right {Q′ = Q} tr) =
case 6-1-3-2 tr of λ where
(inj₁ (.∅ , action , Q∼!a̅∣∅)) →
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ reflexive ∣-cong symmetric ∣-right-identity ⟩
(! a ∙ ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅) ∼⟨ reflexive ∣-cong symmetric Q∼!a̅∣∅ ⟩■
(! a ∙ ∣ ! b ∙) ∣ Q)
, inj₂ (inj₂ (inj₁ refl))
(inj₂ (_ , .∅ , _ , .(co a) , action , a̅[a̅̅]⟶ , _)) →
⊥-elim (names-are-not-inverted a̅[a̅̅]⟶)
rl-lemma (par-τ {Q′ = Q} (par-left {P′ = P} tr₁) tr₂) =
case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
(inj₁ (.∅ , action , P∼!a∣∅) ,
inj₁ (R , tr , Q∼!a̅∣R)) →
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ symmetric ((∣-right-identity ∣-cong reflexive) ∣-cong ∣-right-identity) ⟩
((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ (! co a ∙ ∣ ∅) ∼≡⟨ cong (λ R → _ ∣ (_ ∣ R)) (sym $ ·-only⟶ tr) ⟩
((! a ∙ ∣ ∅) ∣ ! b ∙) ∣ (! co a ∙ ∣ R) ∼⟨ symmetric ((P∼!a∣∅ ∣-cong reflexive) ∣-cong Q∼!a̅∣R) ⟩■
(P ∣ ! b ∙) ∣ Q)
, inj₂ (inj₂ (inj₂ refl))
(inj₂ (() , _) , _)
(_ , inj₂ (() , _))
rl-lemma (par-τ {Q′ = Q} (par-right {Q′ = P} tr₁) tr₂) =
case 6-1-3-2 tr₁ ,′ 6-1-3-2 tr₂ of λ where
(inj₁ (.∅ , action , P∼!b∣∅) ,
inj₁ (R , tr , Q∼!a̅∣R)) →
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ symmetric ((reflexive ∣-cong ∣-right-identity) ∣-cong ∣-right-identity) ⟩
(! a ∙ ∣ (! b ∙ ∣ ∅)) ∣ (! co a ∙ ∣ ∅) ∼≡⟨ cong (λ R → _ ∣ (_ ∣ R)) (sym $ ·-only⟶ tr) ⟩
(! a ∙ ∣ (! b ∙ ∣ ∅)) ∣ (! co a ∙ ∣ R) ∼⟨ symmetric ((reflexive ∣-cong P∼!b∣∅) ∣-cong Q∼!a̅∣R) ⟩■
(! a ∙ ∣ P) ∣ Q)
, inj₂ (inj₂ (inj₂ refl))
(inj₂ (() , _) , _)
(_ , inj₂ (() , _))
rl :
∀ {Q μ} →
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ [ μ ]⟶ Q →
∃ λ P → ! name a ∙ (b ∙) ∣ ! co a ∙ [ μ ]⇒̂ P × [ i ] P ≈′ Q
rl {Q} tr = case rl-lemma tr of λ where
(!a∣!b∣!a̅∼Q , inj₁ refl) →
! name a ∙ (b ∙) ∣ ! co a ∙ →⟨ ⟶: par-left (replication (par-right action)) ⟩■
W.⇒̂[ name a ]
(! name a ∙ (b ∙) ∣ b ∙) ∣ ! co a ∙ ∼⟨ swap-rightmost ⟩
(! name a ∙ (b ∙) ∣ ! co a ∙) ∣ b ∙ ∼′⟨ 6-5-4′ WL.∣-cong′ reflexive ⟩
((! a ∙ ∣ ! b ∙) ∣ ! co a ∙) ∣ b ∙ ∼⟨ swap-rightmost ⟩
((! a ∙ ∣ ! b ∙) ∣ b ∙) ∣ ! co a ∙ ∼⟨ symmetric ∣-assoc ∣-cong reflexive ⟩
(! a ∙ ∣ (! b ∙ ∣ b ∙)) ∣ ! co a ∙ ∼⟨ (reflexive ∣-cong 6-1-2) ∣-cong reflexive ⟩ ∼:
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ !a∣!b∣!a̅∼Q ⟩■
Q
(!a∣!b∣!a̅∼Q , inj₂ (inj₁ refl)) →
! name a ∙ (b ∙) ∣ ! co a ∙ →⟨ par-τ (replication (par-right action))
(replication (par-right action)) ⟩
(! name a ∙ (b ∙) ∣ (b ∙)) ∣ (! co a ∙ ∣ ∅) →⟨ ⟶: par-left (par-right action) ⟩■
W.⇒̂[ name b ]
(! name a ∙ (b ∙) ∣ ∅) ∣ (! co a ∙ ∣ ∅) ∼⟨ ∣-right-identity ∣-cong ∣-right-identity ⟩
(! name a ∙ (b ∙)) ∣ ! co a ∙ ∼′⟨ 6-5-4′ ⟩ ∼:
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ !a∣!b∣!a̅∼Q ⟩■
Q
(!a∣!b∣!a̅∼Q , inj₂ (inj₂ (inj₁ refl))) →
! name a ∙ (b ∙) ∣ ! co a ∙ →⟨ ⟶: par-right (replication (par-right action)) ⟩■
W.⇒̂[ name (co a) ]
! name a ∙ (b ∙) ∣ (! co a ∙ ∣ ∅) ∼⟨ reflexive ∣-cong ∣-right-identity ⟩
! name a ∙ (b ∙) ∣ ! co a ∙ ∼′⟨ 6-5-4′ ⟩ ∼:
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ !a∣!b∣!a̅∼Q ⟩■
Q
(!a∣!b∣!a̅∼Q , inj₂ (inj₂ (inj₂ refl))) →
! name a ∙ (b ∙) ∣ ! co a ∙ ■
W.⇒̂[ τ ]
! name a ∙ (b ∙) ∣ ! co a ∙ ∼′⟨ 6-5-4′ ⟩ ∼:
(! a ∙ ∣ ! b ∙) ∣ ! co a ∙ ∼⟨ !a∣!b∣!a̅∼Q ⟩■
Q
6-5-4′ :
∀ {i a b} →
[ i ] ! name a ∙ (b ∙) ∣ ! co a ∙ ≈′ (! a ∙ ∣ ! b ∙) ∣ ! co a ∙
force 6-5-4′ = 6-5-4
6-5-8-1 :
∀ a {P Q} →
⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) ≳ ⟨ν proj₁ a ⟩ (P ∣ Q)
6-5-8-1 a {P} {Q} = E.⟨ lr , rl ⟩
where
lr :
∀ {μ R} →
⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) [ μ ]⟶ R →
∃ λ R′ → ⟨ν proj₁ a ⟩ (P ∣ Q) [ μ ]⟶̂ R′ × R ≳′ R′
lr (restriction a∉μ (par-left action)) = ⊥-elim (a∉μ refl)
lr (restriction a∉μ (par-right action)) = ⊥-elim (a∉μ refl)
lr (restriction a∉μ (par-τ {Q′ = R} action tr)) =
⟨ν proj₁ a ⟩ (P ∣ R) ∼≡⟨ cong (λ R → ⟨ν _ ⟩ (_ ∣ R)) (·-only⟶ tr) ⟩■
⟨ν proj₁ a ⟩ (P ∣ Q)
⟵̂[ τ ]
⟨ν proj₁ a ⟩ (P ∣ Q) ■
rl :
∀ {μ R′} →
⟨ν proj₁ a ⟩ (P ∣ Q) [ μ ]⟶ R′ →
∃ λ R → ⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) [ μ ]⇒ R ×
R ≳′ R′
rl {μ} (restriction {P′ = R} a∉μ P∣Q⟶R) =
⟨ν proj₁ a ⟩ (name a ∙ P ∣ name (co a) ∙ Q) →⟨ ⟶: restriction _ (par-τ action action) ⟩
⟨ν proj₁ a ⟩ (P ∣ Q) →⟨ ⟶: restriction a∉μ P∣Q⟶R ⟩■
E.⇒[ μ ]
⟨ν proj₁ a ⟩ R ■
¬-6-5-8-2 :
Name →
¬ (∀ {a b P} →
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈
! name b ∙ ⟨ν proj₁ a ⟩ P)
¬-6-5-8-2 x =
(∀ {a b P} →
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈
! name b ∙ ⟨ν proj₁ a ⟩ P) ↝⟨ (λ hyp → hyp {a = a} {b = co a}) ⟩
(! ⟨ν proj₁ a ⟩ (name (co a) ∙ (a ∙) ∣ co a ∙) ≈
! name (co a) ∙ ⟨ν proj₁ a ⟩ ∅) ↝⟨ (λ hyp → Σ-map id proj₁ $ W.right-to-left hyp
(replication (par-right action))) ⟩
∃ (! ⟨ν proj₁ a ⟩ (name (co a) ∙ (a ∙) ∣ co a ∙) [ name (co a) ]⇒̂_) ↝⟨ !P⇒̂ ∘ proj₂ ⟩□
⊥ □
where
a = x , true
P = ⟨ν proj₁ a ⟩ (name (co a) ∙ (a ∙) ∣ co a ∙)
P⟶ : ∀ {μ Q} → ¬ P [ μ ]⟶ Q
P⟶ (restriction x≢x (par-left action)) = ⊥-elim (x≢x refl)
P⟶ (restriction x≢x (par-right action)) = ⊥-elim (x≢x refl)
P⟶ (restriction _ (par-τ action tr)) = names-are-not-inverted tr
!P⟶ : ∀ {μ Q} → ¬ ! P [ μ ]⟶ Q
!P⟶ (replication (par-left tr)) = !P⟶ tr
!P⟶ (replication (par-right tr)) = P⟶ tr
!P⟶ (replication (par-τ _ tr)) = P⟶ tr
!P⇒ : ∀ {Q} → ! P ⇒ Q → Q ≡ ! P
!P⇒ done = refl
!P⇒ (step _ tr _) = ⊥-elim (!P⟶ tr)
!P[]⇒ : ∀ {μ Q} → ¬ ! P [ μ ]⇒ Q
!P[]⇒ (steps trs tr _) rewrite !P⇒ trs = !P⟶ tr
!P⇒̂ : ∀ {b Q} → ¬ ! P [ name b ]⇒̂ Q
!P⇒̂ (silent () _)
!P⇒̂ (non-silent _ tr) = !P[]⇒ tr
6-5-8-2 :
∀ {i a b P} →
proj₁ a ≢ proj₁ b →
[ i ] ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈
! name b ∙ ⟨ν proj₁ a ⟩ P
6-5-8-2 {i} {a} {b} {P} a≢b = W.⟨ lr , rl ⟩
where
6-5-8-2′ :
[ i ] ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ≈′
! name b ∙ ⟨ν proj₁ a ⟩ P
force 6-5-8-2′ = 6-5-8-2 a≢b
lr :
∀ {Q μ} →
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) [ μ ]⟶ Q →
∃ λ Q′ → ! name b ∙ ⟨ν proj₁ a ⟩ P [ μ ]⇒̂ Q′ × [ i ] Q ≈′ Q′
lr {Q} tr = case 6-1-3-2 tr of λ where
(inj₁ (_ , restriction a≢b (par-left action)
, Q∼!νa[ba∣a̅P]∣νa[a∣a̅P])) →
Q ∼⟨ Q∼!νa[ba∣a̅P]∣νa[a∣a̅P] ⟩
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ∣
⟨ν proj₁ a ⟩ (a ∙ ∣ name (co a) ∙ P) ∼⟨ (_ ■) EL.∣-cong 6-5-8-1 _ ⟩
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ∣
⟨ν proj₁ a ⟩ (∅ ∣ P) ∼⟨ 6-5-8-2′ WL.∣-cong′ convert {a = ℓ} (⟨ν refl ⟩-cong ∣-left-identity) ⟩■
! name b ∙ ⟨ν proj₁ a ⟩ P ∣ ⟨ν proj₁ a ⟩ P
W.⇐̂[ name b ] ←⟨ ⟶: replication (par-right action) ⟩■
! name b ∙ ⟨ν proj₁ a ⟩ P
(inj₁ (_ , restriction _ (par-τ action tr) , _)) →
⊥-elim ( $⟨ tr ⟩
name (co a) · _ [ name (co b) ]⟶ _ ↝⟨ ·-only ⟩
name (co a) ≡ name (co b) ↝⟨ cancel-name ⟩
co a ≡ co b ↝⟨ cong proj₁ ⟩
proj₁ a ≡ proj₁ b ↝⟨ a≢b ⟩□
⊥ □)
(inj₁ (_ , restriction a≢a (par-right action) , _)) →
⊥-elim (a≢a refl)
(inj₂ (refl , _ , _ , _
, restriction _ (par-left action)
, restriction _ (par-left tr)
, _)) →
⊥-elim (names-are-not-inverted tr)
(inj₂ (refl , _ , _ , _
, restriction _ (par-right action)
, restriction _ (par-right tr)
, _)) →
⊥-elim (names-are-not-inverted tr)
(inj₂ (refl , _ , _ , _
, restriction a≢b (par-left action)
, restriction _ (par-right tr)
, _)) →
$⟨ tr ⟩
name (co a) ∙ P [ name (co b) ]⟶ _ ↝⟨ cong proj₁ ∘ cancel-name ∘ ·-only ⟩
proj₁ a ≡ proj₁ b ↝⟨ a≢b ⟩
⊥ ↝⟨ ⊥-elim ⟩□
_ □
(inj₂ (refl , _ , _ , c
, restriction a≢c (par-right tr)
, restriction _ (par-left action)
, _)) →
$⟨ tr ⟩
name (co a) ∙ P [ name c ]⟶ _ ↝⟨ cong proj₁ ∘ cancel-name ∘ ·-only ⟩
proj₁ a ≡ proj₁ c ↝⟨ a≢c ⟩
⊥ ↝⟨ ⊥-elim ⟩□
_ □
rl :
∀ {Q′ μ} →
! name b ∙ ⟨ν proj₁ a ⟩ P [ μ ]⟶ Q′ →
∃ λ Q → ! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) [ μ ]⇒̂ Q ×
[ i ] Q ≈′ Q′
rl {Q′} tr = case 6-1-3-2 tr of λ where
(inj₁ (_ , action , Q′∼!bνaP∣νaP)) →
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) →⟨ ⟶: replication (par-right (restriction a≢b (par-left action))) ⟩■
W.⇒̂[ name b ]
! ⟨ν proj₁ a ⟩ (name b ∙ (a ∙) ∣ name (co a) ∙ P) ∣
⟨ν proj₁ a ⟩ (a ∙ ∣ name (co a) ∙ P) ∼′⟨ 6-5-8-2′ WL.∣-cong′ convert {a = ℓ} (6-5-8-1 a) ⟩
! name b ∙ ⟨ν proj₁ a ⟩ P ∣ ⟨ν proj₁ a ⟩ (∅ ∣ P) ∼⟨ (_ ■) ∣-cong ⟨ν refl ⟩-cong ∣-left-identity ⟩ ∼:
! name b ∙ ⟨ν proj₁ a ⟩ P ∣ ⟨ν proj₁ a ⟩ P ∼⟨ symmetric Q′∼!bνaP∣νaP ⟩■
Q′
(inj₂ (refl , _ , _ , _ , action , tr , _)) →
⊥-elim (names-are-not-inverted tr)