Parallel composition

Events are tags: an event of the left component, one of the right, or a label-matched synchronisation. A set of tags is consistent when each component event is consumed once and each projection is consistent in its component, and it enables a tag when each event the tag consumes is enabled in its component.

inductive CCS.Tag {Name : Type u_1} (E : SES (Action Name)) (F : SES (Action Name)) : Type (max u_2 u_3)

A product event: an E-event, an F-event, or a label-matched synchronisation.

• left {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : E.Event → Tag E F
• right {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : F.Event → Tag E F
• sync {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (e : E.Event) (f : F.Event) (h : ∃ (a : Label Name), E.label e = Action.vis a ∧ F.label f = Action.vis a.co) : Tag E F

def CCS.Tag.evL {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : Tag E F → Option E.Event

The E-event a tag consumes.

Equations

• (CCS.Tag.left e).evL = some e
• (CCS.Tag.right a).evL = none
• (CCS.Tag.sync e f h).evL = some e

def CCS.Tag.evR {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : Tag E F → Option F.Event

The F-event a tag consumes.

Equations

• (CCS.Tag.left e).evR = none
• (CCS.Tag.right a).evR = some a
• (CCS.Tag.sync e f h).evR = some f

def CCS.Tag.label {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : Tag E F → Action Name

Synchronisations are silent.

Equations

• (CCS.Tag.left e).label = E.label e
• (CCS.Tag.right a).label = F.label a
• (CCS.Tag.sync e f h).label = CCS.Action.tau

def CCS.projL {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (C : Set (Tag E F)) : Set E.Event

E-events consumed by a set of tags.

Equations

• CCS.projL C = {e : E.Event | ∃ t ∈ C, t.evL = some e}

def CCS.projR {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (C : Set (Tag E F)) : Set F.Event

F-events consumed by a set of tags.

Equations

• CCS.projR C = {f : F.Event | ∃ t ∈ C, t.evR = some f}

theorem CCS.projL_mono {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {C D : Set (Tag E F)} (h : C ⊆ D) : projL C ⊆ projL D

theorem CCS.projR_mono {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {C D : Set (Tag E F)} (h : C ⊆ D) : projR C ⊆ projR D

theorem CCS.projL_union {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (C D : Set (Tag E F)) : projL (C ∪ D) = projL C ∪ projL D

theorem CCS.projR_union {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (C D : Set (Tag E F)) : projR (C ∪ D) = projR C ∪ projR D

theorem CCS.projL_empty {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : projL ∅ = ∅

theorem CCS.projR_empty {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} : projR ∅ = ∅

theorem CCS.projL_singleton {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (t : Tag E F) : projL {t} = {e : E.Event | t.evL = some e}

theorem CCS.projR_singleton {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (t : Tag E F) : projR {t} = {f : F.Event | t.evR = some f}

theorem CCS.projL_finite {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {C : Set (Tag E F)} (h : C.Finite) : (projL C).Finite

theorem CCS.projR_finite {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {C : Set (Tag E F)} (h : C.Finite) : (projR C).Finite

def CCS.ParCon₂ {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (t₁ t₂ : Tag E F) : Prop

Consistency of a pair of tags: no component event consumed twice.

Equations

• CCS.ParCon₂ t₁ t₂ = ((∀ (e : E.Event), t₁.evL = some e → t₂.evL = some e → t₁ = t₂) ∧ ∀ (f : F.Event), t₁.evR = some f → t₂.evR = some f → t₁ = t₂)

def CCS.ParCon {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (X : Finset (Tag E F)) : Prop

Each component event consumed once, and consistent projections.

Equations

• CCS.ParCon X = ((∀ t₁ ∈ X, ∀ t₂ ∈ X, CCS.ParCon₂ t₁ t₂) ∧ E.Consistent (CCS.projL ↑X) ∧ F.Consistent (CCS.projR ↑X))

def CCS.ParEnable {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (X : Finset (Tag E F)) (t : Tag E F) : Prop

Enabling: each consumed event is enabled in its component.

Equations

• One or more equations did not get rendered due to their size.

theorem CCS.exists_cover_L {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {s : Set (Tag E F)} (V : Finset E.Event) (hV : ↑V ⊆ projL s) : ∃ (W : Finset (Tag E F)), ↑W ⊆ s ∧ ↑V ⊆ projL ↑W

A finite set of events covered by a set of tags is covered by finitely many.

theorem CCS.exists_cover_R {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {s : Set (Tag E F)} (V : Finset F.Event) (hV : ↑V ⊆ projR s) : ∃ (W : Finset (Tag E F)), ↑W ⊆ s ∧ ↑V ⊆ projR ↑W

theorem CCS.con_projL {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {s : Set (Tag E F)} (h : ∀ (W : Finset (Tag E F)), ↑W ⊆ s → ParCon W) : E.Consistent (projL s)

Consistency of a set of tags gives consistency of its left projection.

theorem CCS.con_projR {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {s : Set (Tag E F)} (h : ∀ (W : Finset (Tag E F)), ↑W ⊆ s → ParCon W) : F.Consistent (projR s)

theorem CCS.parCon_subset {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {X Y : Finset (Tag E F)} (h : ParCon Y) (hsub : X ⊆ Y) : ParCon X

@[reducible]

def CCS.parSES {Name : Type u_1} (E : SES (Action Name)) (F : SES (Action Name)) : SES (Action Name)

Parallel composition, as a stable event structure.

Equations

• CCS.parSES E F = { Event := CCS.Tag E F, Con := CCS.ParCon, enable := CCS.ParEnable, label := CCS.Tag.label, con_empty := ⋯, con_subset := ⋯, enable_mono := ⋯, enable_inter := ⋯ }

Projections and steps

theorem CCS.projL_eq_pmap {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (c : Set (Tag E F)) : projL c = GES.pmapSet Tag.evL c

theorem CCS.projR_eq_pmap {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} (c : Set (Tag E F)) : projR c = GES.pmapSet Tag.evR c

theorem CCS.projL_isConf {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} (hc : (parSES E F).isConf c) : E.isConf (projL c)

The left projection of a configuration is a configuration.

theorem CCS.projR_isConf {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} (hc : (parSES E F).isConf c) : F.isConf (projR c)

theorem CCS.projL_insert {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} {x : E.Event} (hx : t.evL = some x) : projL (c ∪ {t}) = projL c ∪ {x}

theorem CCS.projL_insert_none {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} (hx : t.evL = none) : projL (c ∪ {t}) = projL c

theorem CCS.projR_insert {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} {y : F.Event} (hy : t.evR = some y) : projR (c ∪ {t}) = projR c ∪ {y}

theorem CCS.projR_insert_none {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} (hy : t.evR = none) : projR (c ∪ {t}) = projR c

theorem CCS.enables_projL {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} {x : E.Event} (hins : (parSES E F).isConf (c ∪ {t})) (hfr : t ∉ c) (hx : t.evL = some x) : E.isConf (projL c ∪ {x}) ∧ x ∉ projL c

Firing a tag fires an enabled, fresh event of each component it consumes.

theorem CCS.enables_projR {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} {y : F.Event} (hins : (parSES E F).isConf (c ∪ {t})) (hfr : t ∉ c) (hy : t.evR = some y) : F.isConf (projR c ∪ {y}) ∧ y ∉ projR c

theorem CCS.isConf_insert_tag {Name : Type u_1} {E : SES (Action Name)} {F : SES (Action Name)} {c : Set (Tag E F)} {t : Tag E F} (hc : (parSES E F).isConf c) (hL : ∀ (x : E.Event), t.evL = some x → E.isConf (projL c ∪ {x}) ∧ x ∉ projL c) (hR : ∀ (y : F.Event), t.evR = some y → F.isConf (projR c ∪ {y}) ∧ y ∉ projR c) : (parSES E F).isConf (c ∪ {t})

A fresh tag whose components are enabled extends a configuration.