def isConf (es : EventStructure) (X : Set es.Event) : Prop

A set of events is a configuration if it is conflict-free and downward closed.

Equations

• isConf es X = ((∀ {e₁ e₂ : es.Event}, e₁ ∈ X → e₂ ∈ X → ¬es.conflict e₁ e₂) ∧ ∀ {e e' : es.Event}, e ∈ X → e' ≤ e → e' ∈ X)

def Conf (es : EventStructure) : Type

Type of all configurations of an event structure.

Equations

• Conf es = { X : Set es.Event // isConf es X }

def FinConf (es : EventStructure) : Type

Type of all finite configurations of an event structure.

Equations

• FinConf es = { X : Finset es.Event // isConf es ↑X }

def Configuration.enables (es : EventStructure) (c : Set es.Event) (e : es.Event) : Prop

A configuration c enables an event e if e is consistent with all events in c and the past of e is contained in c.

Equations

• Configuration.enables es c e = (isConf es c ∧ (∀ e' ∈ c, es.consistent e e') ∧ es.past e ⊆ c)

theorem Configuration.enables_extension (es : EventStructure) {c : Set es.Event} {e : es.Event} (h : enables es c e) : isConf es (c ∪ {e})

If a configuration c enables an event e, then c ∪ {e} is also a configuration.