structure EventStructure : Type (u_1 + 1)

An event structure with binary conflict.

• Event : Type u_1
• poEvent : PartialOrder self.Event
• conflict : self.Event → self.Event → Prop
• conflict_irrefl : Irreflexive self.conflict
• conflict_symm : Symmetric self.conflict
• conflict_hereditary {e₁ e₂ e₃ : self.Event} : self.conflict e₁ e₂ → e₂ ≤ e₃ → self.conflict e₁ e₃

instance EventStructure.instPartialOrderEvent (es : EventStructure) : PartialOrder es.Event

Equations

• es.instPartialOrderEvent = es.poEvent

def EventStructure.consistent (es : EventStructure) (e₁ e₂ : es.Event) : Prop

Consistency relation: two events are consistent if they are not in conflict.

Equations

• es.consistent e₁ e₂ = ¬es.conflict e₁ e₂

theorem EventStructure.consistent_refl (es : EventStructure) : Reflexive es.consistent

Consistency is reflexive.

theorem EventStructure.consistent_symm (es : EventStructure) : Symmetric es.consistent

Consistency is symmetric.

def EventStructure.concurrent (es : EventStructure) (e₁ e₂ : es.Event) : Prop

Concurrency relation: two events are concurrent if they are consistent and causally independent.

Equations

• es.concurrent e₁ e₂ = (es.consistent e₁ e₂ ∧ ¬e₁ ≤ e₂ ∧ ¬e₂ ≤ e₁)

theorem EventStructure.concurrent_irrefl (es : EventStructure) : Irreflexive es.concurrent

Concurrency is irreflexive.

theorem EventStructure.concurrent_symm (es : EventStructure) : Symmetric es.concurrent

Concurrency is symmetric.

def EventStructure.past (es : EventStructure) (e : es.Event) : Set es.Event

The past (downset) of an event: all events causally preceding it.

Equations

• es.past e = {x : es.Event | x ≤ e}

def EventStructure.future (es : EventStructure) (e : es.Event) : Set es.Event

The future (upset) of an event: all events causally succeeding it.

Equations

• es.future e = {x : es.Event | e ≤ x}