Stable event structures

Stability axiom: two enabling sets for the same event, jointly consistent with it, intersect in an enabling set. Causality is still disjunctive, but each event acquires a least history inside a configuration.

structure SES (Label : Type u_1) extends GES Label : Type (max u_1 (u_2 + 1))

A general event structure whose enablings are closed under intersection.

• Event : Type u_2
• Con : Finset self.Event → Prop
• enable : Finset self.Event → self.Event → Prop
• label : self.Event → Label
• con_empty : self.Con ∅
• con_subset {X Y : Finset self.Event} : self.Con Y → X ⊆ Y → self.Con X
• enable_mono {X Y : Finset self.Event} {e : self.Event} : self.enable X e → X ⊆ Y → self.Con Y → self.enable Y e
• enable_inter {X Y Z : Finset self.Event} {e : self.Event} : self.enable X e → self.enable Y e → self.Consistent (↑X ∪ ↑Y ∪ {e}) → ↑Z = ↑X ∩ ↑Y → self.enable Z e

@[reducible]

def SES.toFamily {L : Type u_1} (S : SES L) : ConfFamily L

The configuration family of a stable event structure.

Equations

• S.toFamily = S.toFamily

@[simp]

theorem SES.toFamily_Config {L : Type u_1} (S : SES L) : S.toFamily.Config = S.isConf

theorem SES.inter_isConf {L : Type u_1} {S : SES L} {x y z : Set S.Event} (hx : S.isConf x) (hy : S.isConf y) (hz : S.isConf z) (hxz : x ⊆ z) (hyz : y ⊆ z) : S.isConf (x ∩ y)

Bounded binary intersections of configurations are configurations.

theorem SES.exists_least_enabling {L : Type u_1} {S : SES L} {z : Set S.Event} (hz : S.isConf z) {e : S.Event} {X₀ : Finset S.Event} (hX₀ : S.enable X₀ e) (hX₀z : ↑X₀ ⊆ z) (hez : e ∈ z) : ∃ (M : Finset S.Event), S.enable M e ∧ M ⊆ X₀ ∧ ∀ (Y : Finset S.Event), S.enable Y e → ↑Y ⊆ z → M ⊆ Y

Inside a bound z, an event has a least enabling set.